From 04fbe5e3bb858f0931cfe0b1d9722a8d872ada50 Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Tue, 29 Sep 2020 15:11:18 +0900
Subject: Generalize interval lemmas

- Generalize `mem0_itv(cc|oo)_xNx` and `oppr_itv(|oo|co|oc|cc)` lemmas from
  `numFieldType` to `numDomainType`, which have been specialized in PR #458
  accidentally.
- Generalize `mid_in_itv(|oo|cc)` lemmas from `realFieldType` to `numFieldType`.
---
 mathcomp/algebra/interval.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'mathcomp')

diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v
index d6ea076..067a457 100644
--- a/mathcomp/algebra/interval.v
+++ b/mathcomp/algebra/interval.v
@@ -582,7 +582,7 @@ Import GRing.Theory Num.Theory.
 
 Section IntervalNumDomain.
 
-Variable R : numFieldType.
+Variable R : numDomainType.
 Implicit Types x : R.
 
 Lemma mem0_itvcc_xNx x : (0 \in `[- x, x]) = (0 <= x).
@@ -614,7 +614,7 @@ End IntervalNumDomain.
 
 Section IntervalField.
 
-Variable R : realFieldType.
+Variable R : numFieldType.
 
 Local Notation mid x y := ((x + y) / 2%:R).
 
-- 
cgit v1.2.3