Merge PR #8139: Replace all the CoInductives with Variants in the SSR plugin

3 files changed, 13 insertions, 13 deletions

diff --git a/plugins/ssr/ssrbool.v b/plugins/ssr/ssrbool.v
index 7d05b64384..0865f75ec5 100644
--- a/plugins/ssr/ssrbool.v
+++ b/plugins/ssr/ssrbool.v
@@ -61,8 +61,8 @@ Require Import ssreflect ssrfun.
 (*           classically P <-> we can assume P when proving is_true b.        *)
 (*                         := forall b : bool, (P -> b) -> b.                 *)
 (*                            This is equivalent to ~ (~ P) when P : Prop.    *)
-(*             implies P Q == wrapper coinductive type that coerces to P -> Q *)
-(*                            and can be used as a P -> Q view unambigously.  *)
+(*             implies P Q == wrapper variant type that coerces to P -> Q and *)
+(*                            can be used as a P -> Q view unambigously.      *)
 (*                            Useful to avoid spurious insertion of <-> views *)
 (*                            when Q is a conjunction of foralls, as in Lemma *)
 (*                            all_and2 below; conversely, avoids confusion in *)
@@ -456,7 +456,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.
 
@@ -585,7 +585,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.
 
@@ -603,7 +603,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.
@@ -1119,7 +1119,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]).
 
@@ -1329,7 +1329,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.
@@ -1376,7 +1376,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/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v
index b0a9441385..b4144aa45e 100644
--- a/plugins/ssr/ssreflect.v
+++ b/plugins/ssr/ssreflect.v
@@ -184,7 +184,7 @@ Inductive external_view : Type := tactic_view of Type.
 
 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.
 
@@ -275,10 +275,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.
 Arguments phantom : clear implicits.
 Arguments Phantom : clear implicits.
-CoInductive phant (p : Type) := Phant.
+Variant phant (p : Type) := Phant.
 
 (* Internal tagging used by the implementation of the ssreflect elim.         *)
 
diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v
index ac2c78249b..b2d5143e36 100644
--- a/plugins/ssr/ssrfun.v
+++ b/plugins/ssr/ssrfun.v
@@ -326,7 +326,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.
 
@@ -684,7 +684,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.