Fixing bug #3492.
Regression test for bug #2883.
Regression test #3557
Dead code in inv.ml.
Fixing "simple inversion as" (bug #2164).
Fixing a bug in intros_replacing which was causing inversion not
necessarily granting names given in the "as" clause.
A better check that an "as" clause has been given to inversion, so
that it clears things earlier in the "as" case, allowing
intros_replacing to work without renaming the hypotheses.
(clear_request was not a good idea here a priori, since its use was
not related to the hypothesis to invert but to an hypothesis to inject).
Test for "inversion as" naming bug.
Little fix in documentation of inversion.
Fix bug #3589, unification looping due to incorrect use of stack with primitive projections.
Add a tactic [revgoals] to reverse the list of focused goals.
The [constr:(…)] Ltac construction now shares the same context as [uconstr:(…)].

- The binders names can be influenced by binders defined in Ltac (e.g. [let x:=fresh"y" in let u:=constr:(fun x:nat=>x) in idtac u] ).
- Any untyped constr in the context can now be inserted and type-checked inside a constr. In particular, Gregory Malecha's original proposed syntax for type-checking untyped terms in Ltac is now available [let u:=uconstr:(I I) in let v := constr:(u) in idtac v].
Rename [extract_ltac_uconstr_values] to [extract_ltac_constr_context].

The latter is more representative of its actual function: extract from the Ltac context the values which are relevant to the interpretation of terms (either type or untyped).
CHANGES: binder names from Ltac identifiers.
CHANGES: [Variant], [Set Nonrecursive Elimination Schemes].
Fix [induction] wrt inductive records and non-recursive variants.

- [induction] on inductive records use the generated induction scheme for induction (not destruct as for non-recursive records)
- [induction] on non-recursive variants do destruct as the induction scheme is not generated.
CHANGES: [revgoals].
Doc: [revgoals].
CHANGES: Ltac's [refine] accepts [uconstr].
CHANGES: existential variables are always "substituted" in the new tactic engine.