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.