Fix bug due to shadowing a variable name in tacred
Make constrMatching and detyping more robust with respect to
expand_projection failing if an innapropriate sigma is given.
Add a "Debug Tactic Unification" option and correct the first-order
application case to expand primitive projections at the head of both
applications.
Add debug printers for projections, fix printing of evar constraints
and unsatisfiable constraints which were not done in the right environment.
Give the same argument name for the record binder of type class
projections and regular records.
Easily fixable backwards incompatibility.
Do not expand primitive projections eagerly in evarconv, but only
in cases of unification with existentials requiring it.