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/interval.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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

diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v
index b699da1..80f1b5d 100644
--- a/mathcomp/algebra/interval.v
+++ b/mathcomp/algebra/interval.v
@@ -48,10 +48,10 @@ Local Notation mid x y := ((x + y) / 2%:R).
 
 Section IntervalPo.
 
-CoInductive itv_bound (T : Type) : Type := BOpen_if of bool & T | BInfty.
+Variant itv_bound (T : Type) : Type := BOpen_if of bool & T | BInfty.
 Notation BOpen := (BOpen_if true).
 Notation BClose := (BOpen_if false).
-CoInductive interval (T : Type) := Interval of itv_bound T & itv_bound T.
+Variant interval (T : Type) := Interval of itv_bound T & itv_bound T.
 
 Variable (R : numDomainType).
 
-- 
cgit v1.2.3