Merge pull request #204 from pi8027/replace-coinductive-with-variant

Replace all the CoInductives with Variants

31 files changed, 85 insertions, 85 deletions

diff --git a/mathcomp/algebra/fraction.v b/mathcomp/algebra/fraction.v
index 98eb9f1..28dd82b 100644
--- a/mathcomp/algebra/fraction.v
+++ b/mathcomp/algebra/fraction.v
@@ -53,7 +53,7 @@ Proof. by move=> ny0; rewrite /Ratio /insubd insubT. Qed.
 
 Definition numden_Ratio := (numer_Ratio, denom_Ratio).
 
-CoInductive Ratio_spec (n d : R) : {ratio R} -> R -> R -> Type :=
+Variant Ratio_spec (n d : R) : {ratio R} -> R -> R -> Type :=
   | RatioNull of d = 0 : Ratio_spec n d ratio0 n 0
   | RatioNonNull (d_neq0 : d != 0) : 
     Ratio_spec n d (@mkRatio (n, d) d_neq0) n d.
diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v
index e043561..4c5ad4d 100644
--- a/mathcomp/algebra/intdiv.v
+++ b/mathcomp/algebra/intdiv.v
@@ -560,7 +560,7 @@ Proof. by rewrite coprimezE abszN. Qed.
 Lemma coprimezN m n : coprimez m (- n) = coprimez m n.
 Proof. by rewrite coprimezE abszN. Qed.
 
-CoInductive egcdz_spec m n : int * int -> Type :=
+Variant egcdz_spec m n : int * int -> Type :=
   EgcdzSpec u v of u * m + v * n = gcdz m n & coprimez u v
      : egcdz_spec m n (u, v).
 
diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v
index b699da1..80f1b5d 100644
--- a/mathcomp/algebra/interval.v
+++ b/mathcomp/algebra/interval.v
@@ -48,10 +48,10 @@ Local Notation mid x y := ((x + y) / 2%:R).
 
 Section IntervalPo.
 
-CoInductive itv_bound (T : Type) : Type := BOpen_if of bool & T | BInfty.
+Variant itv_bound (T : Type) : Type := BOpen_if of bool & T | BInfty.
 Notation BOpen := (BOpen_if true).
 Notation BClose := (BOpen_if false).
-CoInductive interval (T : Type) := Interval of itv_bound T & itv_bound T.
+Variant interval (T : Type) := Interval of itv_bound T & itv_bound T.
 
 Variable (R : numDomainType).
 
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v
index ec9fcc5..fca25a9 100644
--- a/mathcomp/algebra/matrix.v
+++ b/mathcomp/algebra/matrix.v
@@ -870,7 +870,7 @@ Proof. by rewrite card_prod !card_ord. Qed.
 Definition mxvec_index (i : 'I_m) (j : 'I_n) :=
   cast_ord mxvec_cast (enum_rank (i, j)).
 
-CoInductive is_mxvec_index : 'I_(m * n) -> Type :=
+Variant is_mxvec_index : 'I_(m * n) -> Type :=
   IsMxvecIndex i j : is_mxvec_index (mxvec_index i j).
 
 Lemma mxvec_indexP k : is_mxvec_index k.
diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v
index d77bfb1..ed8e6c0 100644
--- a/mathcomp/algebra/mxalgebra.v
+++ b/mathcomp/algebra/mxalgebra.v
@@ -1874,7 +1874,7 @@ Section SubDaddsmx.
 Variables m m1 m2 n : nat.
 Variables (A : 'M[F]_(m, n)) (B1 : 'M[F]_(m1, n)) (B2 : 'M[F]_(m2, n)).
 
-CoInductive sub_daddsmx_spec : Prop :=
+Variant sub_daddsmx_spec : Prop :=
   SubDaddsmxSpec A1 A2 of (A1 <= B1)%MS & (A2 <= B2)%MS & A = A1 + A2
                         & forall C1 C2, (C1 <= B1)%MS -> (C2 <= B2)%MS ->
                           A = C1 + C2 -> C1 = A1 /\ C2 = A2.
@@ -1896,7 +1896,7 @@ Section SubDsumsmx.
 
 Variables (P : pred I) (m n : nat) (A : 'M[F]_(m, n)) (B : I -> 'M[F]_n).
 
-CoInductive sub_dsumsmx_spec : Prop :=
+Variant sub_dsumsmx_spec : Prop :=
   SubDsumsmxSpec A_ of forall i, P i -> (A_ i <= B i)%MS
                         & A = \sum_(i | P i) A_ i
                         & forall C, (forall i, P i -> C i <= B i)%MS ->
diff --git a/mathcomp/algebra/polydiv.v b/mathcomp/algebra/polydiv.v
index a3b7ad6..34b6e7b 100644
--- a/mathcomp/algebra/polydiv.v
+++ b/mathcomp/algebra/polydiv.v
@@ -384,7 +384,7 @@ apply: Irec => //; last by rewrite ltn_rmodp.
 by rewrite ltnW // ltn_rmodp.
 Qed.
 
-CoInductive comm_redivp_spec m d : nat * {poly R} * {poly R} -> Type :=
+Variant comm_redivp_spec m d : nat * {poly R} * {poly R} -> Type :=
   ComEdivnSpec k (q r : {poly R}) of
    (GRing.comm d (lead_coef d)%:P -> m * (lead_coef d ^+ k)%:P = q * d + r) &
    (d != 0 -> size r < size d) : comm_redivp_spec m d (k, q, r).
@@ -510,7 +510,7 @@ rewrite -/v -!exprD addnC subnK ?leq_maxl //.
 by rewrite addnC subnK ?subrr ?leq_maxr.
 Qed.
 
-CoInductive rdvdp_spec p q : {poly R} -> bool -> Type :=
+Variant rdvdp_spec p q : {poly R} -> bool -> Type :=
   | Rdvdp k q1 & p * ((lead_coef q)^+ k)%:P = q1 * q : rdvdp_spec p q 0 true
   | RdvdpN & rmodp p q != 0 : rdvdp_spec p q (rmodp p q) false.
 
@@ -727,7 +727,7 @@ Variable R : comRingType.
 
 Implicit Types d p q m n r : {poly R}.
 
-CoInductive redivp_spec (m d : {poly R}) : nat * {poly R} * {poly R} -> Type :=
+Variant redivp_spec (m d : {poly R}) : nat * {poly R} * {poly R} -> Type :=
   EdivnSpec k (q r: {poly R}) of
     (lead_coef d ^+ k) *: m = q * d + r &
    (d != 0 -> size r < size d) : redivp_spec m d (k, q, r).
@@ -870,7 +870,7 @@ Qed.
 
 Hint Resolve lc_expn_scalp_neq0.
 
-CoInductive edivp_spec (m d : {poly R}) :
+Variant edivp_spec (m d : {poly R}) :
                                      nat * {poly R} * {poly R} -> bool -> Type :=
 |Redivp_spec k (q r: {poly R}) of
   (lead_coef d ^+ k) *: m = q * d + r & lead_coef d \notin GRing.unit &
@@ -2340,7 +2340,7 @@ Fixpoint gdcop_rec q p k :=
 
 Definition gdcop q p := gdcop_rec q p (size p).
 
-CoInductive gdcop_spec q p : {poly R} -> Type :=
+Variant gdcop_spec q p : {poly R} -> Type :=
   GdcopSpec r of (dvdp r p) & ((coprimep r q) || (p == 0))
   & (forall d,  dvdp d p -> coprimep d q -> dvdp d r)
   : gdcop_spec q p r.
@@ -3194,7 +3194,7 @@ Qed.
 (* Just to have it without importing the weak theory *)
 Lemma dvdpE p q : p %| q = rdvdp p q. Proof. exact: Idomain.dvdpE. Qed.
 
-CoInductive edivp_spec m d : nat * {poly F} * {poly F} -> Type :=
+Variant edivp_spec m d : nat * {poly F} * {poly F} -> Type :=
   EdivpSpec n q r of
   m = q * d + r & (d != 0) ==> (size r < size d) : edivp_spec m d (n, q, r).
 
diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v
index cd7d306..27f59f5 100644
--- a/mathcomp/algebra/rat.v
+++ b/mathcomp/algebra/rat.v
@@ -150,7 +150,7 @@ Qed.
 
 Fact fracq0  x : fracq (x, 0) = zeroq. Proof. exact/eqP. Qed.
 
-CoInductive fracq_spec (x : int * int) : int * int -> rat -> Type :=
+Variant fracq_spec (x : int * int) : int * int -> rat -> Type :=
   | FracqSpecN of x.2 = 0 : fracq_spec x (x.1, 0) zeroq
   | FracqSpecP k fx of k != 0 : fracq_spec x (k * numq fx, k * denq fx) fx.
 
@@ -418,7 +418,7 @@ Qed.
 Lemma divq_num_den x : (numq x)%:Q / (denq x)%:Q = x.
 Proof. by rewrite -{3}[x]valqK [valq _]surjective_pairing /= fracqE. Qed.
 
-CoInductive divq_spec (n d : int) : int -> int -> rat -> Type :=
+Variant divq_spec (n d : int) : int -> int -> rat -> Type :=
 | DivqSpecN of d = 0 : divq_spec n d n 0 0
 | DivqSpecP k x of k != 0 : divq_spec n d (k * numq x) (k * denq x) x.
 
@@ -436,7 +436,7 @@ move=> dx_neq0 dy_neq0; rewrite -(inj_eq (@mulIf _ (dx * dy) _)) ?mulf_neq0 //.
 by rewrite mulrA divfK // mulrCA divfK // [dx * _ ]mulrC.
 Qed.
 
-CoInductive rat_spec (* (x : rat) *) : rat -> int -> int -> Type :=
+Variant rat_spec (* (x : rat) *) : rat -> int -> int -> Type :=
   Rat_spec (n : int) (d : nat)  & coprime `|n| d.+1
   : rat_spec (* x  *) (n%:Q / d.+1%:Q) n d.+1.
 
diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v
index cbfd593..f12784b 100644
--- a/mathcomp/algebra/ssrint.v
+++ b/mathcomp/algebra/ssrint.v
@@ -48,7 +48,7 @@ Delimit Scope int_scope with Z.
 Local Open Scope int_scope.
 
 (* Defining int *)
-CoInductive int : Set := Posz of nat | Negz of nat.
+Variant int : Set := Posz of nat | Negz of nat.
 (* This must be deferred to module DistInt to work around the design flaws of *)
 (* the Coq module system.                                                     *)
 (* Coercion Posz : nat >-> int. *)
@@ -126,7 +126,7 @@ Qed.
 Definition int_rec := int_rect.
 Definition int_ind := int_rect.
 
-CoInductive int_spec (x : int) : int -> Type :=
+Variant int_spec (x : int) : int -> Type :=
 | ZintNull of x = 0 : int_spec x 0
 | ZintPos n of x = n.+1 : int_spec x n.+1
 | ZintNeg n of x = - (n.+1)%:Z : int_spec x (- n.+1).
@@ -216,7 +216,7 @@ Qed.
 Definition int_rec := int_rect.
 Definition int_ind := int_rect.
 
-CoInductive int_spec (x : int) : int -> Type :=
+Variant int_spec (x : int) : int -> Type :=
 | ZintNull : int_spec x 0
 | ZintPos n : int_spec x n.+1
 | ZintNeg n : int_spec x (- (n.+1)%:Z).
@@ -1438,7 +1438,7 @@ Lemma sgz_cp0 x :
   ((sgz x == 0) = (x == 0)).
 Proof. by rewrite /sgz; case: ltrgtP. Qed.
 
-CoInductive sgz_val x : bool -> bool -> bool -> bool -> bool -> bool
+Variant sgz_val x : bool -> bool -> bool -> bool -> bool -> bool
   -> bool -> bool -> bool -> bool -> bool -> bool
   -> bool -> bool -> bool -> bool -> bool -> bool
   -> R -> R -> int -> Set :=
@@ -1783,4 +1783,4 @@ Lemma rpredXsign R S (divS : @divrPred R S) (kS : keyed_pred divS) n x :
   (x ^ ((-1) ^+ n) \in kS) = (x \in kS).
 Proof. by rewrite -signr_odd; case: (odd n); rewrite ?rpredV. Qed.
 
-End rpred.
\ No newline at end of file
+End rpred.
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index 0d9d135..8d4d3e7 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -1550,15 +1550,15 @@ Proof. exact: rpredD. Qed.
 
 (* dichotomy and trichotomy *)
 
-CoInductive ler_xor_gt (x y : R) : R -> R -> bool -> bool -> Set :=
+Variant ler_xor_gt (x y : R) : R -> R -> bool -> bool -> Set :=
   | LerNotGt of x <= y : ler_xor_gt x y (y - x) (y - x) true false
   | GtrNotLe of y < x  : ler_xor_gt x y (x - y) (x - y) false true.
 
-CoInductive ltr_xor_ge (x y : R) : R -> R -> bool -> bool -> Set :=
+Variant ltr_xor_ge (x y : R) : R -> R -> bool -> bool -> Set :=
   | LtrNotGe of x < y  : ltr_xor_ge x y (y - x) (y - x) false true
   | GerNotLt of y <= x : ltr_xor_ge x y (x - y) (x - y) true false.
 
-CoInductive comparer x y : R -> R ->
+Variant comparer x y : R -> R ->
   bool -> bool -> bool -> bool -> bool -> bool -> Set :=
   | ComparerLt of x < y : comparer x y (y - x) (y - x)
     false false true false true false
@@ -1603,15 +1603,15 @@ have /eqP ->: x == y by rewrite eqr_le le_yx le_xy.
 by rewrite subrr eqxx; constructor.
 Qed.
 
-CoInductive ger0_xor_lt0 (x : R) : R -> bool -> bool -> Set :=
+Variant ger0_xor_lt0 (x : R) : R -> bool -> bool -> Set :=
   | Ger0NotLt0 of 0 <= x : ger0_xor_lt0 x x false true
   | Ltr0NotGe0 of x < 0  : ger0_xor_lt0 x (- x) true false.
 
-CoInductive ler0_xor_gt0 (x : R) : R -> bool -> bool -> Set :=
+Variant ler0_xor_gt0 (x : R) : R -> bool -> bool -> Set :=
   | Ler0NotLe0 of x <= 0 : ler0_xor_gt0 x (- x) false true
   | Gtr0NotGt0 of 0 < x  : ler0_xor_gt0 x x true false.
 
-CoInductive comparer0 x :
+Variant comparer0 x :
                R -> bool -> bool -> bool -> bool -> bool -> bool -> Set :=
   | ComparerGt0 of 0 < x : comparer0 x x false false false true false true
   | ComparerLt0 of x < 0 : comparer0 x (- x) false false true false true false
@@ -3574,7 +3574,7 @@ case: (x =P 0) => [-> | _]; first by rewrite !(eq_sym 0) !signr_eq0 ltrr eqxx.
 by rewrite !(inj_eq signr_inj) eqb_id eqbF_neg signr_eq0 //.
 Qed.
 
-CoInductive sgr_val x : R -> bool -> bool -> bool -> bool -> bool -> bool
+Variant sgr_val x : R -> bool -> bool -> bool -> bool -> bool -> bool
   -> bool -> bool -> bool -> bool -> bool -> bool -> R -> Set :=
   | SgrNull of x = 0 : sgr_val x 0 true true true true false false
     true false false true false false 0
@@ -3760,7 +3760,7 @@ Proof. by move=> x y z; rewrite !minrA [minr x y]minrC. Qed.
 Lemma minrAC : @right_commutative R R min.
 Proof. by move=> x y z; rewrite -!minrA [minr y z]minrC. Qed.
 
-CoInductive minr_spec x y : bool -> bool -> R -> Type :=
+Variant minr_spec x y : bool -> bool -> R -> Type :=
 | Minr_r of x <= y : minr_spec x y true false x
 | Minr_l of y < x : minr_spec x y false true y.
 
@@ -3788,7 +3788,7 @@ Proof. by move=> x y z; rewrite !maxrA [maxr x y]maxrC. Qed.
 Lemma maxrAC : @right_commutative R R max.
 Proof. by move=> x y z; rewrite -!maxrA [maxr y z]maxrC. Qed.
 
-CoInductive maxr_spec x y : bool -> bool -> R -> Type :=
+Variant maxr_spec x y : bool -> bool -> R -> Type :=
 | Maxr_r of y <= x : maxr_spec x y true false x
 | Maxr_l of x < y : maxr_spec x y false true y.
 
@@ -4041,7 +4041,7 @@ Qed.
 Lemma ltr0_sqrtr a : a < 0 -> sqrt a = 0.
 Proof. by move=> /ltrW; apply: ler0_sqrtr. Qed.
 
-CoInductive sqrtr_spec a : R -> bool -> bool -> R -> Type :=
+Variant sqrtr_spec a : R -> bool -> bool -> R -> Type :=
 | IsNoSqrtr of a < 0 : sqrtr_spec a a false true 0
 | IsSqrtr b of 0 <= b : sqrtr_spec a (b ^+ 2) true false b.
 
@@ -4154,7 +4154,7 @@ Let Re2 z := z + z^*.
 Definition nnegIm z := (0 <= imaginaryC * (z^* - z)).
 Definition argCle y z := nnegIm z ==> nnegIm y && (Re2 z <= Re2 y).
 
-CoInductive rootC_spec n (x : C) : Type :=
+Variant rootC_spec n (x : C) : Type :=
   RootCspec (y : C) of if (n > 0)%N then y ^+ n = x else y = 0
                         & forall z, (n > 0)%N -> z ^+ n = x -> argCle y z.
 
diff --git a/mathcomp/character/mxrepresentation.v b/mathcomp/character/mxrepresentation.v
index 4558b3d..c8d7ab1 100644
--- a/mathcomp/character/mxrepresentation.v
+++ b/mathcomp/character/mxrepresentation.v
@@ -1513,7 +1513,7 @@ Qed.
 (* Module isomorphism is an intentional property in general, but it can be    *)
 (* decided when one of the two modules is known to be simple.                 *)
 
-CoInductive mx_iso (U V : 'M_n) : Prop :=
+Variant mx_iso (U V : 'M_n) : Prop :=
   MxIso f of f \in unitmx & (U <= dom_hom_mx f)%MS & (U *m f :=: V)%MS.
 
 Lemma eqmx_iso U V : (U :=: V)%MS -> mx_iso U V.
@@ -1692,7 +1692,7 @@ Qed.
 
 Implicit Type I : finType.
 
-CoInductive mxsemisimple (V : 'M_n) :=
+Variant mxsemisimple (V : 'M_n) :=
   MxSemisimple I U (W := (\sum_(i : I) U i)%MS) of
     forall i, mxsimple (U i) & (W :=: V)%MS & mxdirect W.
 
@@ -1812,7 +1812,7 @@ Qed.
 
 (* Completely reducible modules, and Maeschke's Theorem. *)
 
-CoInductive mxsplits (V U : 'M_n) :=
+Variant mxsplits (V U : 'M_n) :=
   MxSplits (W : 'M_n) of mxmodule W & (U + W :=: V)%MS & mxdirect (U + W).
 
 Definition mx_completely_reducible V :=
@@ -2969,7 +2969,7 @@ Section Similarity.
 Variables (gT : finGroupType) (G : {group gT}).
 Local Notation reprG := (mx_representation F G).
 
-CoInductive mx_rsim n1 (rG1 : reprG n1) n2 (rG2 : reprG n2) : Prop :=
+Variant mx_rsim n1 (rG1 : reprG n1) n2 (rG2 : reprG n2) : Prop :=
   MxReprSim B of n1 = n2 & row_free B
               & forall x, x \in G -> rG1 x *m B = B *m rG2 x.
 
diff --git a/mathcomp/field/algC.v b/mathcomp/field/algC.v
index b045c07..f7cb614 100644
--- a/mathcomp/field/algC.v
+++ b/mathcomp/field/algC.v
@@ -470,7 +470,7 @@ Local Notation Creal := (Num.real : qualifier 0 algC).
 Fact algCi_subproof : {i : algC | i ^+ 2 = -1}.
 Proof. exact: GRing.imaginary_exists. Qed.
 
-CoInductive getCrat_spec : Type := GetCrat_spec CtoQ of cancel QtoC CtoQ.
+Variant getCrat_spec : Type := GetCrat_spec CtoQ of cancel QtoC CtoQ.
 
 Fact getCrat_subproof : getCrat_spec.
 Proof.
diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v
index b43036b..959eea1 100644
--- a/mathcomp/fingroup/fingroup.v
+++ b/mathcomp/fingroup/fingroup.v
@@ -1589,7 +1589,7 @@ Proof. by move=> Gx; rewrite (rcoset_eqP (_ : x \in G :* 1)) mulg1. Qed.
 
 (* Elimination form. *)
 
-CoInductive rcoset_repr_spec x : gT -> Type :=
+Variant rcoset_repr_spec x : gT -> Type :=
   RcosetReprSpec g : g \in G -> rcoset_repr_spec x (g * x).
 
 Lemma mem_repr_rcoset x : repr (G :* x) \in G :* x.
diff --git a/mathcomp/fingroup/gproduct.v b/mathcomp/fingroup/gproduct.v
index 9498de7..986489b 100644
--- a/mathcomp/fingroup/gproduct.v
+++ b/mathcomp/fingroup/gproduct.v
@@ -132,7 +132,7 @@ Proof. by move=> A; rewrite /pprod eqxx. Qed.
 Lemma pprodg1 : right_id 1 pprod.
 Proof. by move=> A; rewrite /pprod eqxx; case: eqP. Qed.
 
-CoInductive are_groups A B : Prop := AreGroups K H of A = K & B = H.
+Variant are_groups A B : Prop := AreGroups K H of A = K & B = H.
 
 Lemma group_not0 G : set0 <> G.
 Proof. by move/setP/(_ 1); rewrite inE group1. Qed.
diff --git a/mathcomp/fingroup/morphism.v b/mathcomp/fingroup/morphism.v
index 32c01d3..3c23921 100644
--- a/mathcomp/fingroup/morphism.v
+++ b/mathcomp/fingroup/morphism.v
@@ -97,7 +97,7 @@ Definition clone_morphism D f :=
 
 Variables (D A : {set aT}) (R : {set rT}) (x : aT) (y : rT) (f : aT -> rT).
 
-CoInductive morphim_spec : Prop := MorphimSpec z & z \in D & z \in A & y = f z.
+Variant morphim_spec : Prop := MorphimSpec z & z \in D & z \in A & y = f z.
 
 Lemma morphimP : reflect morphim_spec (y \in f @: (D :&: A)).
 Proof.
diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v
index ed5d25b..3edcfed 100644
--- a/mathcomp/fingroup/perm.v
+++ b/mathcomp/fingroup/perm.v
@@ -220,7 +220,7 @@ Qed.
 
 Definition tperm x y := perm (can_inj (tperm_proof x y)).
 
-CoInductive tperm_spec x y z : T -> Type :=
+Variant tperm_spec x y z : T -> Type :=
   | TpermFirst of z = x          : tperm_spec x y z y
   | TpermSecond of z = y         : tperm_spec x y z x
   | TpermNone of z <> x & z <> y : tperm_spec x y z z.
diff --git a/mathcomp/fingroup/quotient.v b/mathcomp/fingroup/quotient.v
index 06feab2..03c55b3 100644
--- a/mathcomp/fingroup/quotient.v
+++ b/mathcomp/fingroup/quotient.v
@@ -569,7 +569,7 @@ Variables (G : {group gT}) (Kbar : {group coset_of H}).
 
 Hypothesis nHG : H <| G.
 
-CoInductive inv_quotient_spec (P : pred {group gT}) : Prop :=
+Variant inv_quotient_spec (P : pred {group gT}) : Prop :=
   InvQuotientSpec K of Kbar :=: K / H & H \subset K & P K.
 
 Lemma inv_quotientS :
diff --git a/mathcomp/solvable/frobenius.v b/mathcomp/solvable/frobenius.v
index eb7ceab..98657b4 100644
--- a/mathcomp/solvable/frobenius.v
+++ b/mathcomp/solvable/frobenius.v
@@ -93,7 +93,7 @@ Definition Frobenius_action :=
 
 End FrobeniusAction.
 
-CoInductive has_Frobenius_action G H : Prop :=
+Variant has_Frobenius_action G H : Prop :=
   HasFrobeniusAction sT S to of @Frobenius_action G H sT S to.
 
 End Definitions.
diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v
index 64e8927..2db8927 100644
--- a/mathcomp/ssreflect/bigop.v
+++ b/mathcomp/ssreflect/bigop.v
@@ -525,7 +525,7 @@ Open Scope big_scope.
 (* packages both in in a term in which i occurs; it also depends on the       *)
 (* iterated <op>, as this can give more information on the expected type of   *)
 (* the <general_term>, thus allowing for the insertion of coercions.          *)
-CoInductive bigbody R I := BigBody of I & (R -> R -> R) & bool & R.
+Variant bigbody R I := BigBody of I & (R -> R -> R) & bool & R.
 
 Definition applybig {R I} (body : bigbody R I) x :=
   let: BigBody _ op b v := body in if b then op v x else x.
diff --git a/mathcomp/ssreflect/div.v b/mathcomp/ssreflect/div.v
index 59c19ce..6565ddf 100644
--- a/mathcomp/ssreflect/div.v
+++ b/mathcomp/ssreflect/div.v
@@ -37,7 +37,7 @@ Definition edivn_rec d :=
 
 Definition edivn m d := if d > 0 then edivn_rec d.-1 m 0 else (0, m).
 
-CoInductive edivn_spec m d : nat * nat -> Type :=
+Variant edivn_spec m d : nat * nat -> Type :=
   EdivnSpec q r of m = q * d + r & (d > 0) ==> (r < d) : edivn_spec m d (q, r).
 
 Lemma edivnP m d : edivn_spec m d (edivn m d).
@@ -581,7 +581,7 @@ Fixpoint egcdn_rec m n s qs :=
 
 Definition egcdn m n := Bezout_rec 0 1 (egcdn_rec m n n [::]).
 
-CoInductive egcdn_spec m n : nat * nat -> Type :=
+Variant egcdn_spec m n : nat * nat -> Type :=
   EgcdnSpec km kn of km * m = kn * n + gcdn m n & kn * gcdn m n < m :
     egcdn_spec m n (km, kn).
 
diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v
index 159c00e..01ce7a9 100644
--- a/mathcomp/ssreflect/eqtype.v
+++ b/mathcomp/ssreflect/eqtype.v
@@ -420,7 +420,7 @@ Section FunWith.
 
 Variables (aT : eqType) (rT : Type).
 
-CoInductive fun_delta : Type := FunDelta of aT & rT.
+Variant fun_delta : Type := FunDelta of aT & rT.
 
 Definition fwith x y (f : aT -> rT) := [fun z => if z == x then y else f z].
 
@@ -501,7 +501,7 @@ Definition clone_subType U v :=
 
 Variable sT : subType.
 
-CoInductive Sub_spec : sT -> Type := SubSpec x Px : Sub_spec (Sub x Px).
+Variant Sub_spec : sT -> Type := SubSpec x Px : Sub_spec (Sub x Px).
 
 Lemma SubP u : Sub_spec u.
 Proof. by case: sT Sub_spec SubSpec u => T' _ C rec /= _. Qed.
@@ -514,7 +514,7 @@ Definition insub x :=
 
 Definition insubd u0 x := odflt u0 (insub x).
 
-CoInductive insub_spec x : option sT -> Type :=
+Variant insub_spec x : option sT -> Type :=
   | InsubSome u of P x & val u = x : insub_spec x (Some u)
   | InsubNone   of ~~ P x          : insub_spec x None.
 
diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v
index 4ff769e..6cff46e 100644
--- a/mathcomp/ssreflect/finset.v
+++ b/mathcomp/ssreflect/finset.v
@@ -1197,7 +1197,7 @@ Variables (f : aT -> rT) (f2 : aT -> aT2 -> rT).
 Lemma imsetP D y : reflect (exists2 x, in_mem x D & y = f x) (y \in imset f D).
 Proof. by rewrite [@imset]unlock inE; apply: imageP. Qed.
 
-CoInductive imset2_spec D1 D2 y : Prop :=
+Variant imset2_spec D1 D2 y : Prop :=
   Imset2spec x1 x2 of in_mem x1 D1 & in_mem x2 (D2 x1) & y = f2 x1 x2.
 
 Lemma imset2P D1 D2 y : reflect (imset2_spec D1 D2 y) (y \in imset2 f2 D1 D2).
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index 1446fbd..fec2e35 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
@@ -325,7 +325,7 @@ Prenex Implicits pred0b.
 
 Module FiniteQuant.
 
-CoInductive quantified := Quantified of bool.
+Variant quantified := Quantified of bool.
 
 Delimit Scope fin_quant_scope with Q. (* Bogus, only used to declare scope. *)
 Bind Scope fin_quant_scope with quantified.
@@ -483,7 +483,7 @@ rewrite [enum _](all_pred1P x _ _); first by rewrite size_filter enumP.
 by apply/allP=> y; rewrite mem_enum.
 Qed.
 
-CoInductive pick_spec : option T -> Type :=
+Variant pick_spec : option T -> Type :=
   | Pick x of P x         : pick_spec (Some x)
   | Nopick of P =1 xpred0 : pick_spec None.
 
@@ -938,7 +938,7 @@ Definition arg_min := odflt i0 (pick (arg_pred leq)).
 
 Definition arg_max := odflt i0 (pick (arg_pred geq)).
 
-CoInductive extremum_spec (ord : rel nat) : I -> Type :=
+Variant extremum_spec (ord : rel nat) : I -> Type :=
   ExtremumSpec i of P i & (forall j, P j -> ord (F i) (F j))
     : extremum_spec ord i.
 
@@ -1845,7 +1845,7 @@ Qed.
 Definition unlift n (h i : 'I_n) :=
   omap (fun u : {j | j != h} => Ordinal (unlift_subproof u)) (insub i).
 
-CoInductive unlift_spec n h i : option 'I_n.-1 -> Type :=
+Variant unlift_spec n h i : option 'I_n.-1 -> Type :=
   | UnliftSome j of i = lift h j : unlift_spec h i (Some j)
   | UnliftNone   of i = h        : unlift_spec h i None.
 
@@ -1900,7 +1900,7 @@ Definition split m n (i : 'I_(m + n)) : 'I_m + 'I_n :=
   | GeqNotLtn ge_i_m =>  inr _ (Ordinal (split_subproof ge_i_m))
   end.
 
-CoInductive split_spec m n (i : 'I_(m + n)) : 'I_m + 'I_n -> bool -> Type :=
+Variant split_spec m n (i : 'I_(m + n)) : 'I_m + 'I_n -> bool -> Type :=
   | SplitLo (j : 'I_m) of i = j :> nat     : split_spec i (inl _ j) true
   | SplitHi (k : 'I_n) of i = m + k :> nat : split_spec i (inr _ k) false.
 
diff --git a/mathcomp/ssreflect/generic_quotient.v b/mathcomp/ssreflect/generic_quotient.v
index a3e6cac..16709ee 100644
--- a/mathcomp/ssreflect/generic_quotient.v
+++ b/mathcomp/ssreflect/generic_quotient.v
@@ -213,7 +213,7 @@ Variable qT : quotType T.
 Lemma reprK : cancel repr \pi_qT.
 Proof. by move=> x; rewrite !unlock repr_ofK. Qed.
 
-CoInductive pi_spec (x : T) : T -> Type :=
+Variant pi_spec (x : T) : T -> Type :=
   PiSpec y of x = y %[mod qT] : pi_spec x y.
 
 Lemma piP (x : T) : pi_spec x (repr (\pi_qT x)).
@@ -466,7 +466,7 @@ Lemma right_trans (e : rel T) :
   symmetric e -> transitive e -> right_transitive e.
 Proof. by move=> s t ? * x; rewrite ![e x _]s; apply: left_trans. Qed.
 
-CoInductive equiv_class_of (equiv : rel T) :=
+Variant equiv_class_of (equiv : rel T) :=
   EquivClass of reflexive equiv & symmetric equiv & transitive equiv.
 
 Record equiv_rel := EquivRelPack {
@@ -511,7 +511,7 @@ Section EncodingModuloRel.
 
 Variables (D E : Type) (ED : E -> D) (DE : D -> E) (e : rel D).
 
-CoInductive encModRel_class_of (r : rel D) :=
+Variant encModRel_class_of (r : rel D) :=
   EncModRelClassPack of (forall x, r x x -> r (ED (DE x)) x) & (r =2 e).
 
 Record encModRel := EncModRelPack {
diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v
index e649cbe..94873a8 100644
--- a/mathcomp/ssreflect/path.v
+++ b/mathcomp/ssreflect/path.v
@@ -167,7 +167,7 @@ Section EqPath.
 Variables (n0 : nat) (T : eqType) (x0_cycle : T) (e : rel T).
 Implicit Type p : seq T.
 
-CoInductive split x : seq T -> seq T -> seq T -> Type :=
+Variant split x : seq T -> seq T -> seq T -> Type :=
   Split p1 p2 : split x (rcons p1 x ++ p2) p1 p2.
 
 Lemma splitP p x (i := index x p) :
@@ -177,7 +177,7 @@ move=> p_x; have lt_ip: i < size p by rewrite index_mem.
 by rewrite -{1}(cat_take_drop i p) (drop_nth x lt_ip) -cat_rcons nth_index.
 Qed.
 
-CoInductive splitl x1 x : seq T -> Type :=
+Variant splitl x1 x : seq T -> Type :=
   Splitl p1 p2 of last x1 p1 = x : splitl x1 x (p1 ++ p2).
 
 Lemma splitPl x1 p x : x \in x1 :: p -> splitl x1 x p.
@@ -186,7 +186,7 @@ rewrite inE; case: eqP => [->| _ /splitP[]]; first by rewrite -(cat0s p).
 by split; apply: last_rcons.
 Qed.
 
-CoInductive splitr x : seq T -> Type :=
+Variant splitr x : seq T -> Type :=
   Splitr p1 p2 : splitr x (p1 ++ x :: p2).
 
 Lemma splitPr p x : x \in p -> splitr x p.
@@ -341,7 +341,7 @@ move=> p2'x p2'y; rewrite catA !mem2_cat !mem_cat.
 by rewrite (negPf p2'x) (negPf p2'y) (mem2lf p2'x) andbF !orbF.
 Qed.
 
-CoInductive split2r x y : seq T -> Type :=
+Variant split2r x y : seq T -> Type :=
   Split2r p1 p2 of y \in x :: p2 : split2r x y (p1 ++ x :: p2).
 
 Lemma splitP2r p x y : mem2 p x y -> split2r x y p.
@@ -356,7 +356,7 @@ Fixpoint shorten x p :=
     if x \in p then shorten x p' else y :: shorten y p'
   else [::].
 
-CoInductive shorten_spec x p : T -> seq T -> Type :=
+Variant shorten_spec x p : T -> seq T -> Type :=
    ShortenSpec p' of path e x p' & uniq (x :: p') & subpred (mem p') (mem p) :
      shorten_spec x p (last x p') p'.
 
@@ -870,7 +870,7 @@ rewrite -[p]cat_cons -rot_size_cat rot_uniq => Up.
 by rewrite arc_rot ?left_arc ?mem_head.
 Qed.
 
-CoInductive rot_to_arc_spec p x y :=
+Variant rot_to_arc_spec p x y :=
     RotToArcSpec i p1 p2 of x :: p1 = arc p x y
                           & y :: p2 = arc p y x
                           & rot i p = x :: p1 ++ y :: p2 :
diff --git a/mathcomp/ssreflect/plugin/v8.6/ssrbool.v b/mathcomp/ssreflect/plugin/v8.6/ssrbool.v
index f81e16e..2342ec6 100644
--- a/mathcomp/ssreflect/plugin/v8.6/ssrbool.v
+++ b/mathcomp/ssreflect/plugin/v8.6/ssrbool.v
@@ -442,7 +442,7 @@ Section BoolIf.
 
 Variables (A B : Type) (x : A) (f : A -> B) (b : bool) (vT vF : A).
 
-CoInductive if_spec (not_b : Prop) : bool -> A -> Set :=
+Variant if_spec (not_b : Prop) : bool -> A -> Set :=
   | IfSpecTrue  of      b : if_spec not_b true vT
   | IfSpecFalse of  not_b : if_spec not_b false vF.
 
@@ -577,7 +577,7 @@ Lemma rwP2 : reflect Q b -> (P <-> Q).
 Proof. by move=> Qb; split=> ?; [apply: appP | apply: elimT; case: Qb]. Qed.
 
 (*  Predicate family to reflect excluded middle in bool.                      *)
-CoInductive alt_spec : bool -> Type :=
+Variant alt_spec : bool -> Type :=
   | AltTrue of     P : alt_spec true
   | AltFalse of ~~ b : alt_spec false.
 
@@ -595,7 +595,7 @@ Hint View for apply// equivPif|3 xorPif|3 equivPifn|3 xorPifn|3.
 (* Allow the direct application of a reflection lemma to a boolean assertion. *)
 Coercion elimT : reflect >-> Funclass.
 
-CoInductive implies P Q := Implies of P -> Q.
+Variant implies P Q := Implies of P -> Q.
 Lemma impliesP P Q : implies P Q -> P -> Q. Proof. by case. Qed.
 Lemma impliesPn (P Q : Prop) : implies P Q -> ~ Q -> ~ P.
 Proof. by case=> iP ? /iP. Qed.
@@ -1111,7 +1111,7 @@ Proof. by move=> *; apply/orP; left. Qed.
 Lemma subrelUr r1 r2 : subrel r2 (relU r1 r2).
 Proof. by move=> *; apply/orP; right. Qed.
 
-CoInductive mem_pred := Mem of pred T.
+Variant mem_pred := Mem of pred T.
 
 Definition isMem pT topred mem := mem = (fun p : pT => Mem [eta topred p]).
 
@@ -1321,7 +1321,7 @@ End simpl_mem.
 
 (* Qualifiers and keyed predicates. *)
 
-CoInductive qualifier (q : nat) T := Qualifier of predPredType T.
+Variant qualifier (q : nat) T := Qualifier of predPredType T.
 
 Coercion has_quality n T (q : qualifier n T) : pred_class :=
   fun x => let: Qualifier p := q in p x.
@@ -1368,7 +1368,7 @@ Notation "[ 'qualify' 'an' x : T | P ]" := (Qualifier 2 (fun x : T => P%B))
 Section KeyPred.
 
 Variable T : Type.
-CoInductive pred_key (p : predPredType T) := DefaultPredKey.
+Variant pred_key (p : predPredType T) := DefaultPredKey.
 
 Variable p : predPredType T.
 Structure keyed_pred (k : pred_key p) :=
diff --git a/mathcomp/ssreflect/plugin/v8.6/ssreflect.v b/mathcomp/ssreflect/plugin/v8.6/ssreflect.v
index 860f0a1..e63b45b 100644
--- a/mathcomp/ssreflect/plugin/v8.6/ssreflect.v
+++ b/mathcomp/ssreflect/plugin/v8.6/ssreflect.v
@@ -174,7 +174,7 @@ Notation "T (* n *)" := (abstract T n abstract_key).
 
 Module TheCanonical.
 
-CoInductive put vT sT (v1 v2 : vT) (s : sT) := Put.
+Variant put vT sT (v1 v2 : vT) (s : sT) := Put.
 
 Definition get vT sT v s (p : @put vT sT v v s) := let: Put := p in s.
 
@@ -265,10 +265,10 @@ Notation "{ 'type' 'of' c 'for' s }" := (dependentReturnType c s)
 (*   We also define a simpler version ("phant" / "Phant") of phantom for the  *)
 (* common case where p_type is Type.                                          *)
 
-CoInductive phantom T (p : T) := Phantom.
+Variant phantom T (p : T) := Phantom.
 Implicit Arguments phantom [].
 Implicit Arguments Phantom [].
-CoInductive phant (p : Type) := Phant.
+Variant phant (p : Type) := Phant.
 
 (* Internal tagging used by the implementation of the ssreflect elim.         *)
 
diff --git a/mathcomp/ssreflect/plugin/v8.6/ssrfun.v b/mathcomp/ssreflect/plugin/v8.6/ssrfun.v
index c517b92..7cb30ff 100644
--- a/mathcomp/ssreflect/plugin/v8.6/ssrfun.v
+++ b/mathcomp/ssreflect/plugin/v8.6/ssrfun.v
@@ -419,7 +419,7 @@ Section SimplFun.
 
 Variables aT rT : Type.
 
-CoInductive simpl_fun := SimplFun of aT -> rT.
+Variant simpl_fun := SimplFun of aT -> rT.
 
 Definition fun_of_simpl f := fun x => let: SimplFun lam := f in lam x.
 
@@ -777,7 +777,7 @@ Section Bijections.
 
 Variables (A B : Type) (f : B -> A).
 
-CoInductive bijective : Prop := Bijective g of cancel f g & cancel g f.
+Variant bijective : Prop := Bijective g of cancel f g & cancel g f.
 
 Hypothesis bijf : bijective.
 
diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v
index 648737b..4bbea2a 100644
--- a/mathcomp/ssreflect/prime.v
+++ b/mathcomp/ssreflect/prime.v
@@ -77,7 +77,7 @@ Fixpoint elogn2 e q r {struct q} :=
   | q'.+1, r'.+2 => elogn2 e q' r'
   end.
 
-CoInductive elogn2_spec n : nat * nat -> Type :=
+Variant elogn2_spec n : nat * nat -> Type :=
   Elogn2Spec e m of n = 2 ^ e * m.*2.+1 : elogn2_spec n (e, m).
 
 Lemma elogn2P n : elogn2_spec n.+1 (elogn2 0 n n).
@@ -91,7 +91,7 @@ Qed.
 
 Definition ifnz T n (x y : T) := if n is 0 then y else x.
 
-CoInductive ifnz_spec T n (x y : T) : T -> Type :=
+Variant ifnz_spec T n (x y : T) : T -> Type :=
   | IfnzPos of n > 0 : ifnz_spec n x y x
   | IfnzZero of n = 0 : ifnz_spec n x y y.
 
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index 4347983..e9d29fb 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -305,7 +305,7 @@ Proof. by rewrite -cats1 -catA. Qed.
 Lemma rcons_cat x s1 s2 : rcons (s1 ++ s2) x = s1 ++ rcons s2 x.
 Proof. by rewrite -!cats1 catA. Qed.
 
-CoInductive last_spec : seq T -> Type :=
+Variant last_spec : seq T -> Type :=
   | LastNil        : last_spec [::]
   | LastRcons s x  : last_spec (rcons s x).
 
@@ -1272,7 +1272,7 @@ Proof. by move=> x; rewrite -{2}(cat_take_drop n0 s) !mem_cat /= orbC. Qed.
 Lemma eqseq_rot s1 s2 : (rot n0 s1 == rot n0 s2) = (s1 == s2).
 Proof. by apply: inj_eq; apply: rot_inj. Qed.
 
-CoInductive rot_to_spec s x := RotToSpec i s' of rot i s = x :: s'.
+Variant rot_to_spec s x := RotToSpec i s' of rot i s = x :: s'.
 
 Lemma rot_to s x : x \in s -> rot_to_spec s x.
 Proof.
diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v
index cfe0fa3..4619db7 100644
--- a/mathcomp/ssreflect/ssrnat.v
+++ b/mathcomp/ssreflect/ssrnat.v
@@ -418,7 +418,7 @@ Proof. exact: (@le_irrelevance m.+1). Qed.
 
 (* Comparison predicates. *)
 
-CoInductive leq_xor_gtn m n : bool -> bool -> Set :=
+Variant leq_xor_gtn m n : bool -> bool -> Set :=
   | LeqNotGtn of m <= n : leq_xor_gtn m n true false
   | GtnNotLeq of n < m  : leq_xor_gtn m n false true.
 
@@ -427,21 +427,21 @@ Proof.
 by rewrite ltnNge; case le_mn: (m <= n); constructor; rewrite // ltnNge le_mn.
 Qed.
 
-CoInductive ltn_xor_geq m n : bool -> bool -> Set :=
+Variant ltn_xor_geq m n : bool -> bool -> Set :=
   | LtnNotGeq of m < n  : ltn_xor_geq m n false true
   | GeqNotLtn of n <= m : ltn_xor_geq m n true false.
 
 Lemma ltnP m n : ltn_xor_geq m n (n <= m) (m < n).
 Proof. by rewrite -(ltnS n); case: leqP; constructor. Qed.
 
-CoInductive eqn0_xor_gt0 n : bool -> bool -> Set :=
+Variant eqn0_xor_gt0 n : bool -> bool -> Set :=
   | Eq0NotPos of n = 0 : eqn0_xor_gt0 n true false
   | PosNotEq0 of n > 0 : eqn0_xor_gt0 n false true.
 
 Lemma posnP n : eqn0_xor_gt0 n (n == 0) (0 < n).
 Proof. by case: n; constructor. Qed.
 
-CoInductive compare_nat m n :
+Variant compare_nat m n :
    bool -> bool -> bool -> bool -> bool -> bool -> Set :=
   | CompareNatLt of m < n : compare_nat m n true false true false false false
   | CompareNatGt of m > n : compare_nat m n false true false true false false
@@ -751,7 +751,7 @@ Proof. by case: exP => i Pi; exists (m - i); rewrite subKn ?ubP. Qed.
 
 Definition ex_maxn := m - ex_minn ex_maxn_subproof.
 
-CoInductive ex_maxn_spec : nat -> Type :=
+Variant ex_maxn_spec : nat -> Type :=
   ExMaxnSpec i of P i & (forall j, P j -> j <= i) : ex_maxn_spec i.
 
 Lemma ex_maxnP : ex_maxn_spec ex_maxn.
diff --git a/mathcomp/ssreflect/tuple.v b/mathcomp/ssreflect/tuple.v
index e06bd38..64585f6 100644
--- a/mathcomp/ssreflect/tuple.v
+++ b/mathcomp/ssreflect/tuple.v
@@ -220,7 +220,7 @@ Proof. by []. Qed.
 Lemma tuple0 : all_equal_to ([tuple] : 0.-tuple T).
 Proof. by move=> t; apply: val_inj; case: t => [[]]. Qed.
 
-CoInductive tuple1_spec : n.+1.-tuple T -> Type :=
+Variant tuple1_spec : n.+1.-tuple T -> Type :=
   Tuple1spec x t : tuple1_spec [tuple of x :: t].
 
 Lemma tupleP u : tuple1_spec u.