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.
Documenting the [Variant] type definition and the [Nonrecursive Elimination Schemes] option.
Fix bug #3559, ensuring a canonical order of universe level quantifications when
introducing constants (e.g. Top.1 is always before Top.2), compatible with the one
used before introduction of hMaps in LMap/LSet.
Fix bug #3561, correct folding of env in context[] matching.
Revert "Ltac's [idtac] is now interpreted outside of a goal if possible."

This reverts commit afa441019432f70245fed6adc5eb0318514e4357.
Revert "Ltac's idtac is now implemented using the new API."

This reverts commit 5b92ff7b0a641bf2daa31b60bf49b57a5d1e8452.
Revert "Tacinterp: [interp_message] and associate now only require an environment rather than an entire goal."

This reverts commit 4eaafcd00992302c186b8d11e890616726ebd822.
Revert "Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter]."

This reverts commit 664b3cba1e8d326382ca981aa49fdf00edd429e6.

Conflicts:
	proofs/proofview.ml
Using goal-tactics to interpret arguments to idtac.

This allows to write a multigoal idtac without having to resort to
the hack of modifying the global environment tactic through tclIN_ENV,
which may cause trouble if we want to modify it in a state-passing style.