VernacExtend does not dispatch on type anymore.
Removing "eqn:" for "induction" in reference manual.
Example for apply and evars.
Fixing inversion after having fixed intros_replacing
in69665dd2480d364162933972de7ffa955eccab4d. There are still situations
when "as" is not given where equations coming from injection are not
yet removed, making invalid the computation of dependencies, what
prevents an hypothesis to be cleared and replaced.
More small bugs in intros_replacing.
Fixing localisation of tactic errors (my mistake in himsg.ml essentially).
Fix categorization of recursive inductives.
Fix generation of inductive elimination principle for primitive records.
Let r.(p) be a strict subterm of r during the guardness check.
Parsing and printing of primitive projections, fix buggy behavior when
implicits do not allow to parse as an application and cleanup code.
A step towards better differentiating when w_unify is used for subterm
selection (rewrite, destruct/induction, set or apply on scheme), for
unification (apply on not a scheme, auto), the latter being separated
into primary unification and unification for merging instances.

No change of semantics from within Coq, if I did not mistake (but a
function like secondOrderAbstraction does not set flags by itself
anymore).
Removing remaining documentation of the XML plugin.
Fixing bug #3605.
Fix bug #3505.

When w_unifying primitive projection applications, force
the unification of types of the projected records to recover instances
for the parameters (evarconv does this automatically by unifying evar
instances with their expected type).
Fix bug #3596, wrong treatment of projections in compute_constelim_direct.
Fix bug #3594: eta for constructors and functions at the same time which
was failing in this case due to the wrong postponment of an unsolvable
?X = RigidContext[?X] problem.
Other bugs with "inversion as" (collision between user-provided names and generated equation names).
Keeping a sub-optimal behavior of intros_possibly_replacing for compatibility with inversion