Splitting the uses of the unification function according to the status of
the abs flag in rewrite.
The unifying functions of Rewrite uses the return types of strategies.
More invariants in Rewrite unification.
Removing one Evd.merge in Rewrite.
Rework typeclass resolution and control of backtracking.
Add a global option to check for multiple solutions and fail in that
case.
Add another flag to declare classes as having unique instances (not
checked but assumed correct, avoiding some backtracking).
Fix bug #3621, using fold_left2 on arrays of the same size only.
Fix bug #3610, allowing betaiotadelta reduction while unifying types of
records in unification.ml.
Avoid backtracking in typeclass search if a solution for a closed
non-dependent or propositional constraint has already been found
(same behavior as before previous patch).
Fixing bug #3619 in emacs mode.
A small pass of code cleaning and clenv removing in Rewrite.
Fix a bug in the naming of binders.

The ident closure was not propagated when pretying a [uconstr] coming from a [uconstr] closure. This bug had never been reported, as far as I'm aware.
Fix: when interpreting a identifier in pretying, use the Ltac identifier substitution at the right place.

I used to change [id] to its interpretation before calling [pretype_id]. But it's incorrect: we need to use the Ltac interpretation only when looking up the rel context (where it has been interpreted previously). It would not be to use the interpreted identifier to look up the named context or the Ltac context.
Ltac names in binders: some Ltac values can be seen both as terms and identifiers.

Fixes Ergo.
Fix timing of evar-normalisation  of goals in [Ftactic.nf_enter].

All goals were normalised up front, rather than normalised after the tactic acting on previous goal had the chance to solve some evars, which then appeared non-instantiated to tactics which do not work up to evar map (most of them).
Fixing line break in test for #3559.
Not printing goal name (reinstalled by mistake in a previous commit).
Fixing printing of @eq which was apparently wrong bug fixed by MS on Wed 10.
Adapting ltac output test to new interpretation of binders.
Add a "Hint Mode ref (+ | -)*" hint for setting a global mode
of resulution for goals whose head is "ref". + means the argument
is an input and shouldn't contain an evar, otherwise resolution
fails. This generalizes the Typeclasses Strict Resolution option
which prevents resolution to fire on underconstrained typeclass
constraints, now the criterion can be applied to specific parameters.
Also cleanup auto/eauto code, uncovering a potential backwards
compatibility issue: in cases the goal contains existentials, we
never use the discrimination net in auto/eauto. We should try to
set this on once the contribs are stabilized (the stdlib goes through
when the dnet is used in these cases).
More on printing references applied to implicit arguments.