Removing duplicate clears and turning the warning into an error

11 files changed, 31 insertions, 31 deletions

diff --git a/mathcomp/algebra/Make b/mathcomp/algebra/Make
index 8d89b59..0d0629f 100644
--- a/mathcomp/algebra/Make
+++ b/mathcomp/algebra/Make
@@ -23,6 +23,6 @@ zmodp.v
 -arg -w -arg -projection-no-head-constant
 -arg -w -arg -redundant-canonical-projection
 -arg -w -arg -notation-overridden
--arg -w -arg -duplicate-clear
+-arg -w -arg +duplicate-clear
 -arg -w -arg -ambiguous-paths
 -arg -w -arg +undeclared-scope
diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v
index 336b6df..3efe76d 100644
--- a/mathcomp/algebra/intdiv.v
+++ b/mathcomp/algebra/intdiv.v
@@ -934,7 +934,7 @@ wlog [j a'Mij]: m n M i Da le_mn / {j | ~~ (a %| M i j)%Z}; last first.
     do 2!rewrite /cofactor [row' _ _]mx11_scalar !mxE det_scalar1 /=.
     rewrite mulr1 mul1r mulN1r opprK -[_ + _](mulzK _ nz_b) mulrDl.
     by rewrite -!mulrA !divzK ?dvdz_gcdl ?dvdz_gcdr // Db divzz nz_b unitr1.
-  have{Db} Db: M1 i 0 = b.
+  have{} Db: M1 i 0 = b.
     rewrite /M1 -(lshift0 n 1) [U]block_mxEh mul_mx_row row_mxEl.
     rewrite -[M](@hsubmxK _ _ 2) (@mul_row_col _ _ 2) mulmx0 addr0 !mxE /=.
     rewrite big_ord_recl big_ord1 !mxE /= [lshift _ _]((_ =P 0) _) // Da.
@@ -943,7 +943,7 @@ wlog [j a'Mij]: m n M i Da le_mn / {j | ~~ (a %| M i j)%Z}; last first.
   exists L => //; exists (R *m invmx U); last exists d => //.
     by rewrite unitmx_mul uR unitmx_inv.
   by rewrite mulmxA -dM1 mulmxK.
-move=> {A leA IHa} IHa; wlog Di: i M Da / i = 0; last rewrite {i}Di in Da.
+move=> {A leA}IHa; wlog Di: i M Da / i = 0; last rewrite {i}Di in Da.
   case/(_ 0 (xrow i 0 M)); rewrite ?mxE ?tpermR // => L uL [R uR [d dvD dM]].
   exists (xrow i 0 L); first by rewrite xrowE unitmx_mul unitmx_perm.
   exists R => //; exists d; rewrite //= xrowE -!mulmxA (mulmxA L) -dM xrowE.
@@ -982,7 +982,7 @@ without loss{nz_a a_dvM} a1: M a Da / a = 1.
   by rewrite !nth_default ?size_map ?mulr0.
 rewrite {a}a1 -[m.+1]/(1 + m)%N -[n.+1]/(1 + n)%N in M Da *.
 pose Mu := ursubmx M; pose Ml := dlsubmx M.
-have{Da} Da: ulsubmx M = 1 by rewrite [_ M]mx11_scalar !mxE !lshift0 Da.
+have{} Da: ulsubmx M = 1 by rewrite [_ M]mx11_scalar !mxE !lshift0 Da.
 pose M1 := - (Ml *m Mu) + drsubmx M.
 have [|L uL [R uR [d dvD dM1]]] := IHmn m n M1; first by rewrite -addnS ltnW.
 exists (block_mx 1 0 Ml L).
@@ -1023,7 +1023,7 @@ have [L _ [G uG [D _ defK]]] := int_Smith_normal_form K.
 pose Gud := castmx (Dm, Em) G; pose G'lr := castmx (Em, Dm) (invmx G).
 have{K L D defK kerK} kerGu: map_mx intr (usubmx Gud) *m S = 0.
   pose Kl : 'M[rat]_k:= map_mx intr (lsubmx (castmx (Ek, Dm) (K *m invmx G))).
-  have{defK} defK: map_mx intr K = row_mx Kl 0 *m map_mx intr Gud.
+  have{} defK: map_mx intr K = row_mx Kl 0 *m map_mx intr Gud.
     rewrite -[K](mulmxKV uG) -{2}[G](castmxK Dm Em) -/Gud.
     rewrite -[K *m _](castmxK Ek Dm) map_mxM map_castmx.
     rewrite -(hsubmxK (castmx _ _)) map_row_mx -/Kl map_castmx /Em.
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v
index 77d2e4f..9b27ba7 100644
--- a/mathcomp/algebra/matrix.v
+++ b/mathcomp/algebra/matrix.v
@@ -1650,7 +1650,7 @@ Lemma diagmx_ind (P : forall m n, 'M_(m, n) -> Type) :
   forall m n A, is_diag_mx A -> P m n A.
 Proof.
 move=> P0l P0r PS m n A Adiag; have Atrig := is_diag_mx_is_trig Adiag.
-elim/trigmx_ind: Atrig Adiag => // {m n} m n r c {A}A _ PA.
+elim/trigmx_ind: Atrig Adiag => // {}m {}n r c {}A _ PA.
 rewrite is_diag_block_mx => // /and4P[_ /eqP-> _ Adiag].
 exact: PS (PA _).
 Qed.
@@ -1660,7 +1660,7 @@ Lemma diagsqmx_ind (P : forall n, 'M[V]_n -> Type) :
   (forall n x c A, is_diag_mx A -> P n A -> P (1 + n)%N (block_mx x 0 c A)) ->
   forall n A, is_diag_mx A -> P n A.
 Proof.
-move=> P0 PS n A; elim/sqmx_ind: A => {n} [|n x r c] A PA.
+move=> P0 PS n A; elim/sqmx_ind: A => [|{}n x r c] A PA.
   by rewrite thinmx0; apply: P0.
 rewrite is_diag_block_mx => // /and4P[/eqP-> /eqP-> _ Adiag].
 exact: PS (PA _).
diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v
index cc3c6c6..dde8843 100644
--- a/mathcomp/algebra/mxalgebra.v
+++ b/mathcomp/algebra/mxalgebra.v
@@ -885,7 +885,7 @@ Lemma eq_genmx m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
   (A :=: B -> <<A>> = <<B>>)%MS.
 Proof.
 move=> eqAB; rewrite unlock.
-have{eqAB} eqAB: equivmx A (row_full A) =1 equivmx B (row_full B).
+have{} eqAB: equivmx A (row_full A) =1 equivmx B (row_full B).
   by move=> C; rewrite /row_full /equivmx !eqAB.
 rewrite (eq_choose eqAB) (choose_id _ (genmx_witnessP B)) //.
 by rewrite -eqAB genmx_witnessP.
@@ -1379,7 +1379,7 @@ Let capmx_norm_eq m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
   qidmx A = qidmx B -> (A == B)%MS -> capmx_norm A = capmx_norm B.
 Proof.
 move=> eqABid /eqmxP eqAB.
-have{eqABid eqAB} eqAB: equivmx A (qidmx A) =1 equivmx B (qidmx B).
+have{eqABid} eqAB: equivmx A (qidmx A) =1 equivmx B (qidmx B).
   by move=> C; rewrite /equivmx eqABid !eqAB.
 rewrite {1}/capmx_norm (eq_choose eqAB).
 by apply: choose_id; first rewrite -eqAB; apply: capmx_witnessP.
diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v
index 19a23e6..625be60 100644
--- a/mathcomp/algebra/mxpoly.v
+++ b/mathcomp/algebra/mxpoly.v
@@ -175,13 +175,13 @@ have{Ss u} ->: Ss = Ss_ dS.
   apply/matrixP=> i j; rewrite mxE [in X in _ = X]mxE; case: (j == j0) => {j}//.
   apply/polyP=> k; rewrite coef_poly Sylvester_mxE mxE.
   have [k_ge_dS | k_lt_dS] := leqP dS k.
-    case: (split i) => {i}i; rewrite !mxE coefMXn;
+    case: (split i) => {}i; rewrite !mxE coefMXn;
     case: ifP => // /negbT; rewrite -ltnNge ltnS => hi.
       apply: (leq_sizeP _ _ (leqnn (size p))); rewrite -(ltn_predK p_nc).
       by rewrite ltn_subRL (leq_trans _ k_ge_dS) // ltn_add2r.
     - apply: (leq_sizeP _ _ (leqnn (size q))); rewrite -(ltn_predK q_nc).
       by rewrite ltn_subRL (leq_trans _ k_ge_dS) // addnC ltn_add2l.
-  by rewrite insubdK //; case: (split i) => {i}i;
+  by rewrite insubdK //; case: (split i) => {}i;
      rewrite !mxE coefMXn; case: leqP.
 case: (ubnPgeq dS) (dS_gt0); elim=> // dj IHj ltjS _; pose j1 := Ordinal ltjS.
 pose rj0T (A : 'M[{poly R}]_dS) := row j0 A^T.
@@ -253,7 +253,7 @@ have le_q'_dq: size q' <= dq.
   by rewrite /dq -(size_scale q nz_k) q'r size_mul // addnC -def_r leq_addl.
 exists (row_mx (- c *: poly_rV q') (k *: poly_rV p')).
   apply: contraNneq r_nz; rewrite -row_mx0; case/eq_row_mx=> q0 p0.
-  have{p0} p0: p = 0.
+  have{} p0: p = 0.
     apply/eqP; rewrite -size_poly_eq0 -(size_scale p nz_c) p'r.
     rewrite -(size_scale _ nz_k) scalerAl -(poly_rV_K le_p'_dp) -linearZ p0.
     by rewrite linear0 mul0r size_poly0.
diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v
index e3de209..c413171 100644
--- a/mathcomp/algebra/poly.v
+++ b/mathcomp/algebra/poly.v
@@ -2510,7 +2510,7 @@ have [|q' def_q] := factor_theorem q z _; last first.
   by exists q'; rewrite big_cons mulrA -def_q.
 rewrite {p}def_p in rpz.
 elim/last_ind: rs drs rpz => [|rs t IHrs] /=; first by rewrite big_nil mulr1.
-rewrite all_rcons => /andP[/andP[/eqP czt Uzt] /IHrs {IHrs}IHrs].
+rewrite all_rcons => /andP[/andP[/eqP czt Uzt] /IHrs{}IHrs].
 rewrite -cats1 big_cat big_seq1 /= mulrA rootE hornerM_comm; last first.
   by rewrite /comm_poly hornerXsubC mulrBl mulrBr czt.
 rewrite hornerXsubC -opprB mulrN oppr_eq0 -(mul0r (t - z)).
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.
diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v
index 455a79e..fa952bb 100644
--- a/mathcomp/algebra/ssralg.v
+++ b/mathcomp/algebra/ssralg.v
@@ -4233,22 +4233,22 @@ Proof.
 suffices eq0_ring t1: rformula (eq0_rform t1) by elim: f => //= => f1 ->.
 rewrite /eq0_rform; move: (ub_var t1) => m; set tr := _ m.
 suffices: all rterm (tr.1 :: tr.2).
-  case: tr => {t1} t1 r /= /andP[t1_r].
+  case: tr => {}t1 r /= /andP[t1_r].
   by elim: r m => [|t r IHr] m; rewrite /= ?andbT // => /andP[->]; apply: IHr.
 have: all rterm [::] by [].
 rewrite {}/tr; elim: t1 [::] => //=.
 - move=> t1 IHt1 t2 IHt2 r.
-  move/IHt1; case: to_rterm => {t1 r IHt1} t1 r /= /andP[t1_r].
-  move/IHt2; case: to_rterm => {t2 r IHt2} t2 r /= /andP[t2_r].
+  move/IHt1; case: to_rterm => {r IHt1}t1 r /= /andP[t1_r].
+  move/IHt2; case: to_rterm => {r IHt2}t2 r /= /andP[t2_r].
   by rewrite t1_r t2_r.
 - by move=> t1 IHt1 r /IHt1; case: to_rterm.
 - by move=> t1 IHt1 n r /IHt1; case: to_rterm.
 - move=> t1 IHt1 t2 IHt2 r.
-  move/IHt1; case: to_rterm => {t1 r IHt1} t1 r /= /andP[t1_r].
-  move/IHt2; case: to_rterm => {t2 r IHt2} t2 r /= /andP[t2_r].
+  move/IHt1; case: to_rterm => {r IHt1}t1 r /= /andP[t1_r].
+  move/IHt2; case: to_rterm => {r IHt2}t2 r /= /andP[t2_r].
   by rewrite t1_r t2_r.
 - move=> t1 IHt1 r.
-  by move/IHt1; case: to_rterm => {t1 r IHt1} t1 r /=; rewrite all_rcons.
+  by move/IHt1; case: to_rterm => {r IHt1}t1 r /=; rewrite all_rcons.
 - by move=> t1 IHt1 n r /IHt1; case: to_rterm.
 Qed.
 
@@ -4317,7 +4317,7 @@ elim: t r0 m => /=; try do [
   by move=> n r m hlt hub; rewrite take_size (ltn_addr _ hlt) rsub_id
 | by move=> n r m hlt hub; rewrite leq0n take_size rsub_id
 | move=> t1 IHt1 t2 IHt2 r m; rewrite geq_max; case/andP=> hub1 hub2 hmr;
-  case: to_rterm {IHt1 hub1 hmr}(IHt1 r m hub1 hmr) => t1' r1;
+  case: to_rterm {hub1 hmr}(IHt1 r m hub1 hmr) => t1' r1;
   case=> htake1 hub1' hsub1 <-;
   case: to_rterm {IHt2 hub2 hsub1}(IHt2 r1 m hub2 hsub1) => t2' r2 /=;
   rewrite geq_max; case=> htake2 -> hsub2 /= <-;
@@ -4327,8 +4327,8 @@ elim: t r0 m => /=; try do [
    first by [rewrite takel_cat // -htake1 size_take geq_min leqnn orbT];
   rewrite -(rsub_acc r1 r3 t1') {hub1'}// -{htake1}htake2 {r3}cat_take_drop;
   by elim: r2 m => //= u r2 IHr2 m; rewrite IHr2
-| do [ move=> t1 IHt1 r m; do 2!move/IHt1=> {IHt1}IHt1
-     | move=> t1 IHt1 n r m; do 2!move/IHt1=> {IHt1}IHt1];
+| do [ move=> t1 IHt1 r m; do 2!move=> /IHt1{}IHt1
+     | move=> t1 IHt1 n r m; do 2!move=> /IHt1{}IHt1];
   case: to_rterm IHt1 => t1' r1 [-> -> hsub1 <-]; split=> {hsub1}//;
   by elim: r1 m => //= u r1 IHr1 m; rewrite IHr1].
 move=> t1 IH r m letm /IH {IH} /(_ letm) {letm}.
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) //;
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index 7da7ebc..4bb7a5a 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -3468,7 +3468,7 @@ pose cmp_mu s := [pred i | s * mu < s * En i].
 have{Enonconstant} has_cmp_mu e (s := (-1) ^+ e): {i | i \in A & cmp_mu s i}.
   apply/sig2W/exists_inP; apply: contraR Enonconstant => /exists_inPn-mu_s_A.
   have n_gt0 i: i \in A -> (0 < n)%N by rewrite [n](cardD1 i) => ->.
-  have{mu_s_A} mu_s_A i: i \in A -> s * En i <= s * mu.
+  have{} mu_s_A i: i \in A -> s * En i <= s * mu.
     move=> Ai; rewrite real_leNgt ?mu_s_A ?rpredMsign ?ger0_real ?Ege0 //.
     by rewrite -(pmulrn_lge0 _ (n_gt0 i Ai)) -sumrMnl sumr_ge0.
   have [_ /esym/eqfun_inP] := leif_sum (fun i Ai => leif_eq (mu_s_A i Ai)).
@@ -4305,7 +4305,7 @@ Qed.
 
 Lemma sqrtrM a b : 0 <= a -> sqrt (a * b) = sqrt a * sqrt b.
 Proof.
-case: (sqrtrP a) => // {a} a a_ge0 _; case: (sqrtrP b) => [b_lt0 | {b} b b_ge0].
+case: (sqrtrP a) => // {}a a_ge0 _; case: (sqrtrP b) => [b_lt0 | {}b b_ge0].
   by rewrite mulr0 ler0_sqrtr // nmulr_lle0 ?mulr_ge0.
 by rewrite mulrACA sqrtr_sqr ger0_norm ?mulr_ge0.
 Qed.
@@ -4415,7 +4415,7 @@ have sz_p: size p = n.+1.
   rewrite size_addl ?size_polyXn // ltnS size_opp size_polyC mulrn_eq0.
   by case: posnP => //; case: negP.
 pose r := sort argCle r0; have r_arg: sorted argCle r by apply: sort_sorted.
-have{Dp} Dp: p = \prod_(z <- r) ('X - z%:P).
+have{} Dp: p = \prod_(z <- r) ('X - z%:P).
   rewrite Dp lead_coefE sz_p coefB coefXn coefC -mulrb -mulrnA mulnb lt0n andNb.
   by rewrite subr0 eqxx scale1r; apply/esym/perm_big; rewrite perm_sort.
 have mem_rP z: (n > 0)%N -> reflect (z ^+ n = x) (z \in r).
diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v
index e02aaef..76bec6f 100644
--- a/mathcomp/algebra/vector.v
+++ b/mathcomp/algebra/vector.v
@@ -1101,7 +1101,7 @@ Lemma free_span X v (sumX := fun k => \sum_(x <- X) k x *: x) :
 Proof.
 rewrite -{2}[X]in_tupleE => freeX /coord_span def_v.
 pose k x := oapp (fun i => coord (in_tuple X) i v) 0 (insub (index x X)).
-exists k => [|k1 {def_v}def_v _ /(nthP 0)[i ltiX <-]].
+exists k => [|k1 {}def_v _ /(nthP 0)[i ltiX <-]].
   rewrite /sumX (big_nth 0) big_mkord def_v; apply: eq_bigr => i _.
   by rewrite /k index_uniq ?free_uniq // valK.
 rewrite /k /= index_uniq ?free_uniq // insubT //= def_v.
@@ -1627,7 +1627,7 @@ Proof. by apply: (iffP subvP) => cUf x /cUf/fixedSpaceP. Qed.
 Lemma fixedSpace_limg f U : (U <= fixedSpace f -> f @: U = U)%VS.
 Proof.
 move/fixedSpacesP=> cUf; apply/vspaceP=> x.
-by apply/memv_imgP/idP=> [[{x} x Ux ->] | Ux]; last exists x; rewrite ?cUf.
+by apply/memv_imgP/idP=> [[{}x Ux ->] | Ux]; last exists x; rewrite ?cUf.
 Qed.
 
 Lemma fixedSpace_id : fixedSpace \1 = {:vT}%VS.
@@ -1862,7 +1862,7 @@ Lemma sumv_pi_uniq_sum v :
   \sum_(i <- r0 | P i) sumv_pi_for defV i v = v.
 Proof.
 rewrite /sumv_pi_for defV -!(big_filter r0 P).
-elim: (filter P r0) v => [|i r IHr] v /= => [_ | /andP[r'i /IHr{IHr}IHr]].
+elim: (filter P r0) v => [|i r IHr] v /= => [_ | /andP[r'i /IHr{}IHr]].
   by rewrite !big_nil memv0 => /eqP.
 rewrite !big_cons eqxx => /addv_pi1_pi2; congr (_ + _ = v).
 rewrite -[_ v]IHr ?memv_pi2 //; apply: eq_big_seq => j /=.