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/algebra/fraction.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp/algebra/fraction.v')

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