Replace all the CoInductives with Variants

[pi8027]

The MathComp library uses many CoInductive commands to build non-recursive type families without generating inductive principles. I think that it

• confuses beginners and reviewers not familiar with MathComp,
• makes extracted OCaml programs slower, and
• can be replaced with Variant commands (see https://coq.inria.fr/refman/language/gallina-specification-language.html#coq:cmd.variant).

This patch simply replaces all the CoInductive commands with Variant commands in the current master branch. This works well with Coq 8.8.1 in my environment. I will prepare the same pull requests for coq/coq (the Ssreflect plugin) and math-comp/odd-order if everyone agrees with this modification.

[CohenCyril]

I think this is a good idea, but AFAIK, the Variant vernac is available only for 8.8, so we should wait a few versions of Coq before integrating.

[pi8027]

The Variant command has been available since Coq 8.5beta1 (CHANGES). Currently, MathComp supports only Coq 8.6, 8.7, and 8.8. This change passed CI checks. So I think there is no need to wait.

[CohenCyril]

Oh right! My mistake