From e1d5e9c2585bad2e9c27a476276761cc71ff9c91 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt
Date: Tue, 19 Jan 2021 01:36:20 +0900
Subject: fixes #694

---
 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 4a1cadb..b6964f1 100644
--- a/mathcomp/algebra/interval.v
+++ b/mathcomp/algebra/interval.v
@@ -217,9 +217,9 @@ Proof. by rewrite /<=%O /= lteifxx. Qed.
 Lemma bound_ltxx c1 c2 x : (BSide c1 x < BSide c2 x) = (c1 && ~~ c2).
 Proof. by rewrite /<%O /= lteifxx. Qed.
 
-Lemma ge_pinftyE b : (+oo <= b) = (b == +oo). Proof. by move: b => [|[]]. Qed.
+Lemma ge_pinfty b : (+oo <= b) = (b == +oo). Proof. by move: b => [|[]]. Qed.
 
-Lemma le_ninftyE b : (b <= -oo) = (b == -oo). Proof. by case: b => // - []. Qed.
+Lemma le_ninfty b : (b <= -oo) = (b == -oo). Proof. by case: b => // - []. Qed.
 
 Lemma gt_pinfty b : (+oo < b) = false. Proof. by []. Qed.
 
-- 
cgit v1.2.3