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

(limited to 'mathcomp/ssreflect/tuple.v')

diff --git a/mathcomp/ssreflect/tuple.v b/mathcomp/ssreflect/tuple.v
index e06bd38..64585f6 100644
--- a/mathcomp/ssreflect/tuple.v
+++ b/mathcomp/ssreflect/tuple.v
@@ -220,7 +220,7 @@ Proof. by []. Qed.
 Lemma tuple0 : all_equal_to ([tuple] : 0.-tuple T).
 Proof. by move=> t; apply: val_inj; case: t => [[]]. Qed.
 
-CoInductive tuple1_spec : n.+1.-tuple T -> Type :=
+Variant tuple1_spec : n.+1.-tuple T -> Type :=
   Tuple1spec x t : tuple1_spec [tuple of x :: t].
 
 Lemma tupleP u : tuple1_spec u.
-- 
cgit v1.2.3