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

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

diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v
index 7945265..3db328d 100644
--- a/mathcomp/algebra/rat.v
+++ b/mathcomp/algebra/rat.v
@@ -294,7 +294,7 @@ Proof. by move=> x y /=; rewrite !ratz_frac mulq_frac // /= !mulr1. Qed.
 Fact invq_frac x :
   x.1 != 0 -> x.2 != 0 -> invq (fracq x) = fracq (invq_subdef x).
 Proof.
-by rewrite /invq_subdef; case: fracqP => // k {x} x k0; rewrite fracqMM.
+by rewrite /invq_subdef; case: fracqP => // k {}x k0; rewrite fracqMM.
 Qed.
 
 Fact mulqC : commutative mulq.
@@ -357,7 +357,7 @@ Canonical rat_countFieldType := [countFieldType of rat].
 
 Lemma numq_eq0 x : (numq x == 0) = (x == 0).
 Proof.
-rewrite -[x]valqK fracq_eq0; case: fracqP=> /= [|k {x} x k0].
+rewrite -[x]valqK fracq_eq0; case: fracqP=> /= [|k {}x k0].
   by rewrite eqxx orbT.
 by rewrite !mulf_eq0 (negPf k0) /= denq_eq0 orbF.
 Qed.
-- 
cgit v1.2.3