Replace all the CoInductives with Variants

5 files changed, 5 insertions, 5 deletions

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 :