From 10171942883948c8144ec076ef48eb73f8e49cdd Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Thu, 12 Jul 2018 20:19:55 +0900
Subject: Replace all the CoInductives with Variants

---
 mathcomp/field/algC.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp/field')

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.
-- 
cgit v1.2.3