diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/algebra/interval.v | 4 |
1 files changed, 2 insertions, 2 deletions
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). |