From e565f8d9bebd4fd681c34086d5448dbaebc11976 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Thu, 19 Nov 2020 18:33:21 +0100
Subject: Removing duplicate clears and turning the warning into an error

---
 mathcomp/algebra/ssrint.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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

diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v
index aa899b2..e234504 100644
--- a/mathcomp/algebra/ssrint.v
+++ b/mathcomp/algebra/ssrint.v
@@ -410,7 +410,7 @@ Proof. by case: m; first case. Qed.
 
 Lemma subz_ge0 m n : lez 0 (n - m) = lez m n.
 Proof.
-case: (intP m); case: (intP n)=> // {m n} m n /=;
+case: (intP m); case: (intP n)=> // {}m {}n /=;
 rewrite ?ltnS -?opprD ?opprB ?subzSS; case: leqP=> // hmn;
 by [ rewrite subzn //
    | rewrite -opprB subzn ?(ltnW hmn) //;
-- 
cgit v1.2.3