Merge pull request #658 from CohenCyril/duplicate_clear

Removing duplicate clears and turning the warning into an error

10 files changed, 26 insertions, 26 deletions

diff --git a/mathcomp/field/Make b/mathcomp/field/Make
index c906bd9..93795e9 100644
--- a/mathcomp/field/Make
+++ b/mathcomp/field/Make
@@ -15,6 +15,6 @@ separable.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
\ No newline at end of file
diff --git a/mathcomp/field/algC.v b/mathcomp/field/algC.v
index 815bfba..68e1ba7 100644
--- a/mathcomp/field/algC.v
+++ b/mathcomp/field/algC.v
@@ -71,14 +71,14 @@ have nz2: 2%:R != 0 :> L.
   apply/eqP=> char2; apply: conj_nt => e; apply/eqP/idPn=> eJ.
   have opp_id x: - x = x :> L.
     by apply/esym/eqP; rewrite -addr_eq0 -mulr2n -mulr_natl char2 mul0r.
-  have{char2} char2: 2 \in [char L] by apply/eqP.
+  have{} char2: 2 \in [char L] by apply/eqP.
   without loss{eJ} eJ: e / conj e = e + 1.
     move/(_ (e / (e + conj e))); apply.
     rewrite fmorph_div rmorphD conjK -{1}[conj e](addNKr e) mulrDl.
     by rewrite opp_id (addrC e) divff // addr_eq0 opp_id.
   pose a := e * conj e; have aJ: conj a = a by rewrite rmorphM conjK mulrC.
   have [w Dw] := @solve_monicpoly _ 2 (nth 0 [:: e * a; - 1]) isT.
-  have{Dw} Dw: w ^+ 2 + w = e * a.
+  have{} Dw: w ^+ 2 + w = e * a.
     by rewrite Dw !big_ord_recl big_ord0 /= mulr1 mulN1r addr0 subrK.
   pose b := w + conj w; have bJ: conj b = b by rewrite rmorphD conjK addrC.
   have Db2: b ^+ 2 + b = a.
diff --git a/mathcomp/field/algebraics_fundamentals.v b/mathcomp/field/algebraics_fundamentals.v
index a950ecc..c956047 100644
--- a/mathcomp/field/algebraics_fundamentals.v
+++ b/mathcomp/field/algebraics_fundamentals.v
@@ -239,7 +239,7 @@ without loss{nCq} qx0: q mon_q q_dv_p / root (q ^ FtoL) x.
   rewrite -(subnn (size q1)) {1}IHq1 ?Dp ?dvdp_mulr // polySpred ?monic_neq0 //.
   by rewrite eqSS size_monicM ?monic_neq0 // -!subn1 subnAC addKn.
 have /dvdp_prod_XsubC[m Dq]: q ^ FtoL %| p_ I by rewrite DpI dvdp_map.
-pose B := [set j in mask m (enum I)]; have{Dq} Dq: q ^ FtoL = p_ B.
+pose B := [set j in mask m (enum I)]; have{} Dq: q ^ FtoL = p_ B.
   apply/eqP; rewrite -eqp_monic ?monic_map ?monic_prod_XsubC //.
   congr (_ %= _): Dq; apply: perm_big => //.
   by rewrite uniq_perm ?mask_uniq ?enum_uniq // => j; rewrite mem_enum inE.
@@ -372,7 +372,7 @@ pose root_in (xR : realC) p := exists2 w, w \in sQ (tag xR) & root p w.
 pose extendsR (xR yR : realC) := tag xR \in sQ (tag yR).
 have add_Rroot xR p c: {yR | extendsR xR yR & has_Rroot xR p c -> root_in yR p}.
   rewrite {}/extendsR; case: (has_Rroot xR p c) / and4P; last by exists xR.
-  case: xR => x [R QxR] /= [/inQpK <-]; move: (p ^ _) => {p}p mon_p /inQ_K<- Dc.
+  case: xR => x [R QxR] /= [/inQpK <-]; move: (p ^ _) => {}p mon_p /inQ_K<- Dc.
   have{c Dc} p0_le0: (p ^ QxR).[0] <= 0.
     rewrite horner_coef0 coef_map -[p`_0]ofQ_K -coef_map -horner_coef0 (eqP Dc).
     by rewrite -rmorphX -rmorphN ofQ_K /= rmorphN rmorphX oppr_le0 sqr_ge0.
@@ -417,7 +417,7 @@ have add_Rroot xR p c: {yR | extendsR xR yR & has_Rroot xR p c -> root_in yR p}.
   exists u => {s s_y}//; set y := ofQ z (t_ u); set p1 := minPoly Qx u in Dp.
   have /QtoQ[Qyz QyzE]: y \in sQ z := sQof z (t_ u).
   pose q1_ v := Fadjoin_poly Qx u (Qyz v).
-  have{QyzE} QyzE v: Qyz v = (q1_ v).[u].
+  have{} QyzE v: Qyz v = (q1_ v).[u].
     by rewrite Fadjoin_poly_eq // -Dt -sQof2 QyzE sQof.
   have /all_sig2[q_ coqp Dq] v: {q | v != 0 -> coprimep p q & q ^ Qxz = q1_ v}.
     have /pQwx[q Dq]: q1_ v \is a polyOver Qx by apply: Fadjoin_polyOver.
@@ -572,7 +572,7 @@ have add_Rroot xR p c: {yR | extendsR xR yR & has_Rroot xR p c -> root_in yR p}.
     have /(find_root ((d * e)^-1 *: r ^ QxR))[N ub_rp] := xab0.
     pose f := d * e * h2; apply/posP; exists (maxn N (maxn m n)), f => [|k].
       by rewrite !mulr_gt0 ?invr_gt0 ?ltr0n.
-    rewrite !geq_max => /and3P[/ab_le/ub_rp{ub_rp}ub_rp le_mk le_nk].
+   rewrite !geq_max => /and3P[/ab_le/ub_rp{}ub_rp le_mk le_nk].
     rewrite -(ltr_add2r f) -mulr2n -mulr_natr divfK // /nlim /lim Dqvw.
     rewrite rmorphD hornerD /= -addrA -ltr_subl_addl ler_lt_add //.
       by rewrite rmorphM hornerM ler_pmul ?ltW ?v_gtd ?w_gte.
diff --git a/mathcomp/field/algnum.v b/mathcomp/field/algnum.v
index bed8e71..0b1e892 100644
--- a/mathcomp/field/algnum.v
+++ b/mathcomp/field/algnum.v
@@ -392,7 +392,7 @@ have ext1 mu0 x: {mu1 | exists y, x = Sinj mu1 y
     suffices in01M: lrmorphism in01 by exists (LRMorphism in01M).
     pose rwM := (=^~ Din01, SinjZ, rmorph1, rmorphB, rmorphM).
     by do 3?split; try move=> ? ?; apply: (fmorph_inj QrC); rewrite !rwM.
-  have {z zz Dz px Dx} Dx: exists xx, x = QrC xx.
+  have {z zz Dz px} Dx: exists xx, x = QrC xx.
     exists (map_poly (in_alg Qr) px).[zz].
     by rewrite -horner_map Dz Sinj_poly Dx.
   pose lin01 := linfun in01; pose K := (lin01 @: fullv)%VS.
@@ -637,7 +637,7 @@ Proof.
 have ZP_C c: (ZtoC c)%:P \is a polyOver Cint by rewrite raddfMz rpred_int.
 move=> mulS S_P x Sx; pose v := \row_(i < n) Y`_i.
 have [v0 | nz_v] := eqVneq v 0.
-  case/S_P: Sx => {x}x ->; rewrite big1 ?isAlgInt0 // => i _.
+  case/S_P: Sx => {}x ->; rewrite big1 ?isAlgInt0 // => i _.
   by have /rowP/(_ i) := v0; rewrite !mxE => ->; rewrite mul0rz.
 have sYS (i : 'I_n): x * Y`_i \in S.
   by rewrite rpredM //; apply/S_P/Cint_spanP/mem_Cint_span/memt_nth.
diff --git a/mathcomp/field/closed_field.v b/mathcomp/field/closed_field.v
index 266788c..24b764b 100644
--- a/mathcomp/field/closed_field.v
+++ b/mathcomp/field/closed_field.v
@@ -538,7 +538,7 @@ elim: t; do ?[ by move=> * //=; do ?case: (_ == _)].
 - by move=> t irt /= n rt; rewrite rpoly_map_mul ?irt //.
 - move=> t irt s irs /=; case/andP=> rt rs.
   by apply: rmulpT; rewrite ?irt ?irs //.
-- move=> t irt /= n rt; move: (irt rt)=> {rt} rt; elim: n => [|n ihn] //=.
+- move=> t irt /= n rt; move: (irt rt) => {}rt; elim: n => [|n ihn] //=.
   exact: rmulpT.
 Qed.
 
@@ -886,7 +886,7 @@ suffices{Kclosed} algF_K: {FtoK : {rmorphism F -> Kfield} | integralRange FtoK}.
   pose Kdec := DecFieldType Kfield (closed_field_QEMixin Kclosed).
   pose KclosedField := ClosedFieldType Kdec Kclosed.
   by exists [countClosedFieldType of CountType KclosedField cntK].
-exists (EtoKM 0%N) => /= z; have [i [{z}z ->]] := KtoE z.
+exists (EtoKM 0%N) => /= z; have [i [{}z ->]] := KtoE z.
 suffices{z} /(_ z)[p mon_p]: integralRange (toE 0%N i isT).
   by rewrite -(fmorph_root (EtoKM i)) -map_poly_comp toEtoKp; exists p.
 rewrite /toE /E; clear - minXp_gt1 ext1root ext1gen.
diff --git a/mathcomp/field/cyclotomic.v b/mathcomp/field/cyclotomic.v
index 5359cce..a6ba3bc 100644
--- a/mathcomp/field/cyclotomic.v
+++ b/mathcomp/field/cyclotomic.v
@@ -234,7 +234,7 @@ without loss{nz_af} [mon_f mon_g]: af f g Df Dfg / f \is monic /\ g \is monic.
   - by rewrite rmorphMz -scalerMzr scalerMzl -mulrzA cfg1.
   - by rewrite mulrzAl mulrzAr -mulrzA cfg1.
   by rewrite !(intz, =^~ scaler_int) !monicE !lead_coefZ mulrC cfg1.
-have{af Df} Df: pQtoC pf = pZtoC f.
+have{af} Df: pQtoC pf = pZtoC f.
   have:= congr1 lead_coef Df.
   rewrite lead_coefZ lead_coef_map_inj //; last exact: intr_inj.
   rewrite !(monicP _) // mulr1 Df => <-; rewrite scale1r -map_poly_comp.
@@ -289,7 +289,7 @@ suffices: coprimep (pZtoC f) (pZtoC (g \Po 'X^p)).
 suffices: coprimep f (g \Po 'X^p).
   case/Bezout_coprimepP=> [[u v]]; rewrite -size_poly_eq1.
   rewrite -(size_map_inj_poly (can_inj intCK)) // rmorphD !rmorphM /=.
-  rewrite size_poly_eq1 => {co_fg}co_fg; apply/Bezout_coprimepP.
+  rewrite size_poly_eq1 => {}co_fg; apply/Bezout_coprimepP.
   by exists (pZtoC u, pZtoC v).
 apply: contraLR co_fg => /coprimepPn[|d]; first exact: monic_neq0.
 rewrite andbC -size_poly_eq1 dvdp_gcd => /and3P[sz_d].
diff --git a/mathcomp/field/fieldext.v b/mathcomp/field/fieldext.v
index d99b69b..9091dd8 100644
--- a/mathcomp/field/fieldext.v
+++ b/mathcomp/field/fieldext.v
@@ -680,7 +680,7 @@ rewrite rootM => pqx0 szpq.
 have [nzq nzp]: q != 0 /\ p != 0.
   by apply/norP; rewrite -mulf_eq0 -size_poly_eq0 szpq.
 without loss{pqx0} qx0: q p Kp Kq nzp nzq szpq / root q x.
-  move=> IH; case/orP: pqx0 => /IH{IH}IH; first exact: IH.
+  move=> IH; case/orP: pqx0 => /IH{}IH; first exact: IH.
   have{IH} /orP[]: (q %= p * q) || (q %= 1) by apply: IH => //; rewrite mulrC.
     by rewrite orbC -{1}[q]mul1r eqp_mul2r // eqp_sym => ->.
   by rewrite -{1}[p]mul1r eqp_sym eqp_mul2r // => ->.
@@ -875,7 +875,7 @@ Implicit Types (V : {vspace L}) (E : {subfield L}).
 
 Lemma trivial_fieldOver : (1%VS : {vspace L_F}) =i F.
 Proof.
-move=> x; apply/vlineP/idP=> [[{x}x ->] | Fx].
+move=> x; apply/vlineP/idP=> [[{}x ->] | Fx].
   by rewrite fieldOver_scaleE mulr1 (valP x).
 by exists (vsproj F x); rewrite fieldOver_scaleE mulr1 vsprojK.
 Qed.
@@ -912,7 +912,7 @@ suff: basis_of (vspaceOver M) b by apply: size_basis.
 apply/andP; split.
   rewrite eqEsubv; apply/andP; split; apply/span_subvP=> u.
     by rewrite mem_vspaceOver field_module_eq // => /Mb.
-  move/(@vbasis_mem _ _ _ M); rewrite -defM => /memv_sumP[{u}u Fu ->].
+  move/(@vbasis_mem _ _ _ M); rewrite -defM => /memv_sumP[{}u Fu ->].
   apply: memv_suml => i _; have /memv_cosetP[a Fa ->] := Fu i isT.
   by apply: (memvZ (Subvs Fa)); rewrite memv_span ?memt_nth.
 apply/freeP=> a /(directv_sum_independent dx_b) a_0 i.
@@ -1109,7 +1109,7 @@ move=> v; rewrite -{1}(field_module_eq modM0) -(mem_vspaceOver M0) {}/V.
 move: (vspaceOver F1 M0) => M.
 apply/idP/idP=> [/coord_vbasis|/coord_span]->; apply/memv_suml=> i _.
   rewrite /(_ *: _) /= /fieldOver_scale; case: (coord _ i _) => /= x.
-  rewrite {1}[F1]unlock mem_baseVspace => /vlineP[{x}x ->].
+  rewrite {1}[F1]unlock mem_baseVspace => /vlineP[{}x ->].
   by rewrite -(@scalerAl F L) mul1r memvZ ?memv_span ?memt_nth.
 move: (coord _ i _) => x; rewrite -[_`_i]mul1r scalerAl -tnth_nth.
 have F1x: x%:A \in F1.
diff --git a/mathcomp/field/finfield.v b/mathcomp/field/finfield.v
index 492aed8..19684dc 100644
--- a/mathcomp/field/finfield.v
+++ b/mathcomp/field/finfield.v
@@ -405,7 +405,7 @@ have fZ: linear f.
 have /kAut_to_gal[alpha galLalpha Dalpha]: kAut 1 {:L} (linfun (Linear fZ)).
   rewrite kAutfE; apply/kHomP; split=> [x y _ _ | x /idfP]; rewrite !lfunE //=.
   exact: (rmorphM (RMorphism fM)).
-have{Dalpha} Dalpha: alpha =1 f by move=> a; rewrite -Dalpha ?memvf ?lfunE.
+have{} Dalpha: alpha =1 f by move=> a; rewrite -Dalpha ?memvf ?lfunE.
 suffices <-: fixedField [set alpha] = 1%AS.
   by rewrite gal_generated /generator; exists alpha.
 apply/vspaceP=> x; apply/fixedFieldP/idfP; rewrite ?memvf // => id_x.
@@ -442,7 +442,7 @@ End FinGalois.
 Lemma Fermat's_little_theorem (L : fieldExtType F) (K : {subfield L}) a :
   (a \in K) = (a ^+ order K == a).
 Proof.
-move: K a; wlog [{L}L -> K a]: L / exists galL : splittingFieldType F, L = galL.
+move: K a; wlog [{}L -> K a]: L / exists galL : splittingFieldType F, L = galL.
   by pose galL := (FinSplittingFieldType F L) => /(_ galL); apply; exists galL.
 have /galois_fixedField fixLK := finField_galois (subvf K).
 have [alpha defGalLK Dalpha] := finField_galois_generator (subvf K).
diff --git a/mathcomp/field/galois.v b/mathcomp/field/galois.v
index 82c4819..f41ec06 100644
--- a/mathcomp/field/galois.v
+++ b/mathcomp/field/galois.v
@@ -158,7 +158,7 @@ Definition kHom_rmorphism K E f homKEf :=
 Lemma kHom_horner K E f p x :
   kHom K E f -> p \is a polyOver E -> x \in E -> f p.[x] = (map_poly f p).[f x].
 Proof.
-move=> homKf /polyOver_subvs[{p}p -> Ex]; pose fRM := kHom_rmorphism homKf.
+move=> homKf /polyOver_subvs[{}p -> Ex]; pose fRM := kHom_rmorphism homKf.
 by rewrite (horner_map _ _ (Subvs Ex)) -[f _](horner_map fRM) map_poly_comp.
 Qed.
 
@@ -632,7 +632,7 @@ have [f homLf fxz]: exists2 f : 'End(Lz), kHom 1 imL f & f (inLz x) = z.
   pose f0 := kHomExtend 1 \1 (inLz x) z.
   have{map1q1z_z} hom_f0 : kHom 1 <<1; inLz x>> f0.
     by apply: kHomExtendP map1q1z_z => //; apply: kHom1.
-  have{splitLpz} splitLpz: splittingFieldFor <<1; inLz x>> pz imL.
+  have{} splitLpz: splittingFieldFor <<1; inLz x>> pz imL.
     have [r def_pz defLz] := splitLpz; exists r => //.
     apply/eqP; rewrite eqEsubv -{2}defLz adjoin_seqSl ?sub1v // andbT.
     apply/Fadjoin_seqP; split; last first.
@@ -1230,7 +1230,7 @@ exists (pmap f r).
 rewrite splitKa; have{splitKa}: all (root (minPoly K a)) r.
   by apply/allP => b; rewrite splitKa root_prod_XsubC.
 elim: r Er => /= [|b r IHr]; first by rewrite !big_nil.
-case/andP=> Eb Er /andP[pKa_b_0 /(IHr Er){IHr Er}IHr].
+case/andP=> Eb Er /andP[pKa_b_0 /(IHr Er){Er}IHr].
 have [x galE /eqP xa_b] := normalField_root_minPoly sKE nKE Ea pKa_b_0.
 rewrite /(f b); case: (pickP _) => [y /andP[_ /eqP<-]|/(_ x)/andP[]//].
 by rewrite !big_cons IHr.
@@ -1587,7 +1587,7 @@ Proof. by rewrite -normalField_ker ker_normal. Qed.
 Lemma normalField_img : normalField_cast @* 'Gal(E / K) = 'Gal(M / K).
 Proof.
 have [[sKM sME] [sKE _ nKE]] := (andP sKME, and3P galKE).
-apply/setP=> x; apply/idP/idP=> [/morphimP[{x}x galEx _ ->] | galMx].
+apply/setP=> x; apply/idP/idP=> [/morphimP[{}x galEx _ ->] | galMx].
   rewrite gal_kHom //; apply/kAHomP=> a Ka; have Ma := subvP sKM a Ka.
   by rewrite normalField_cast_eq // (fixed_gal sKE).
 have /(kHom_to_gal sKME nKE)[y galEy eq_xy]: kHom K M x by rewrite -gal_kHom.
diff --git a/mathcomp/field/separable.v b/mathcomp/field/separable.v
index e51a660..6320343 100644
--- a/mathcomp/field/separable.v
+++ b/mathcomp/field/separable.v
@@ -414,7 +414,7 @@ exists p => //; exists (\poly_(i < r.+1) f`_(i * p)).
 rewrite comp_polyE size_poly_eq -?Dn ?fn1 ?oner_eq0 //.
 have pr_p := charf_prime charLp; have p_gt0 := prime_gt0 pr_p.
 apply/polyP=> i; rewrite coef_sum.
-have [[{i} i ->] | p'i] := altP (@dvdnP p i); last first.
+have [[{}i ->] | p'i] := altP (@dvdnP p i); last first.
   rewrite big1 => [|j _]; last first.
     rewrite coefZ -exprM coefXn [_ == _](contraNF _ p'i) ?mulr0 // => /eqP->.
     by rewrite dvdn_mulr.
@@ -512,7 +512,7 @@ Lemma Derivation_separableP :
     (separable_element K x).
 Proof.
 apply: (iffP idP) => [sepKx D derD /subvP DK_0 | derKx_0].
-  have{DK_0} DK_0 q: q \is a polyOver K -> map_poly D q = 0.
+  have{} DK_0 q: q \is a polyOver K -> map_poly D q = 0.
     move=> /polyOverP Kq; apply/polyP=> i; apply/eqP.
     by rewrite coef0 coef_map -memv_ker DK_0.
   apply/subvP=> _ /Fadjoin_polyP[p Kp ->]; rewrite memv_ker.
@@ -771,7 +771,7 @@ have sep_pKy: separable_poly (minPoly K y).
 have{sep_pKy} sep_q: separable_poly q by rewrite Dq separable_map in sep_pKy.
 have [r nz_r PETr] := large_field_PET nz_p px0 qy0 sep_q.
 have [[s [Us Ks /ltnW leNs]] | //] := finite_PET (size r).
-have{s Us leNs} /allPn[t {Ks}/Ks Kt nz_rt]: ~~ all (root r) s.
+have{s Us leNs} /allPn[t {}/Ks Kt nz_rt]: ~~ all (root r) s.
   by apply: contraTN leNs; rewrite -ltnNge => /max_poly_roots->.
 have{PETr} [/= [p1 Dx] [q1 Dy]] := PETr (Subvs Kt) nz_rt.
 set z := t * y - x in Dx Dy; exists z; apply/eqP.