Replace all the CoInductives with Variants

9 files changed, 32 insertions, 32 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.