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

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

diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v
index e043561..4c5ad4d 100644
--- a/mathcomp/algebra/intdiv.v
+++ b/mathcomp/algebra/intdiv.v
@@ -560,7 +560,7 @@ Proof. by rewrite coprimezE abszN. Qed.
 Lemma coprimezN m n : coprimez m (- n) = coprimez m n.
 Proof. by rewrite coprimezE abszN. Qed.
 
-CoInductive egcdz_spec m n : int * int -> Type :=
+Variant egcdz_spec m n : int * int -> Type :=
   EgcdzSpec u v of u * m + v * n = gcdz m n & coprimez u v
      : egcdz_spec m n (u, v).
 
-- 
cgit v1.2.3