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

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

diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v
index ec9fcc5..fca25a9 100644
--- a/mathcomp/algebra/matrix.v
+++ b/mathcomp/algebra/matrix.v
@@ -870,7 +870,7 @@ Proof. by rewrite card_prod !card_ord. Qed.
 Definition mxvec_index (i : 'I_m) (j : 'I_n) :=
   cast_ord mxvec_cast (enum_rank (i, j)).
 
-CoInductive is_mxvec_index : 'I_(m * n) -> Type :=
+Variant is_mxvec_index : 'I_(m * n) -> Type :=
   IsMxvecIndex i j : is_mxvec_index (mxvec_index i j).
 
 Lemma mxvec_indexP k : is_mxvec_index k.
-- 
cgit v1.2.3