Replace all the CoInductives with Variants

14 files changed, 42 insertions, 42 deletions

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.