Print error messages with more hidden information based on α-equivalence .

The comparison on terms which triggers new printing flags in case two terms which are different would be printed identically now contains α-equivalence.

The implementation using a canonization function on [constr] instead of trying to deal with [constr_expr] was suggested by Hugo.
Code simplification in Tacenv.
Useless hooks in Tacintern.
Fixing bug #2818.

Local Ltac definitions do not register their name in the nametab anymore,
thus elegantly solving the bug. The tactic body remains accessible from
the tactic engine, but the name is rendered meaningless to the userside.
Test-suite for bug #2818.
Fixing printing of unreachable local tactics.
Yes another remaining clearing bug with 'apply in'.
Putting back normalized goals when entering them.

This should allow tactics after a Goal.enter not to have to renormalize
them uselessly.
Fix bug #3563, making syntactic matching of primitive projections
and their eta-expanded forms succeed, potentially filling parameter
metavariables from the type information of the projected object.
Add test suite files for closed bugs.
Add test-suite file for Case derivation on primitive records.
Add a [Variant] declaration which allows to write non-recursive variant types.

Just like the [Record] keyword allows only non-recursive records.
Print [Variant] types with the keyword [Variant].

Involves changing the [mind_finite] field in the kernel from a bool to the trivalued type [Decl_kinds.recursivity_kind]. This is why so many files are (unfortunately) affected. It would not be very surprising if some bug was introduced.
Types declared as Variants really do not accept recursive definitions.
Inductive and CoInductive records are printed correctly.
Type definitions [Variant] and [Record] really don't accept the wrong kind of definition.

- [Variant] will accept variant definitions but no record definition
- [Record] will accept record definitions but no variant definition
Type definitions with [Variant] don't generate inductive schemes by default.

- The option [Record Elimination Schemes] is replaced by [Nonrecursive Elimination Schemes] ([Record Elimination Schemes] is kept as a deprecated option for compatibility)
- [Variant] don't generate inductive scheme unless [Nonrecursive Elimination Schemes] is turned on.
- Inductive records generate induction schemes even when [Nonrecursive Elimination Schemes] is off.
Remove [Infer] option of records.

Dead code formerly used by the now defunct [autoinstances].
Factorize the parsing rules of [Record] and the other kind of type definitions.

They were almost identical, except some unused misplaced coercion symbol in the non-[Record] rule.
Commands like [Inductive > X := … | … | …] raise an error message instead of silently ignoring the ">" syntax.