Removing duplicate clears and turning the warning into an error

9 files changed, 16 insertions, 16 deletions

diff --git a/mathcomp/solvable/Make b/mathcomp/solvable/Make
index fd00057..2f5aac3 100644
--- a/mathcomp/solvable/Make
+++ b/mathcomp/solvable/Make
@@ -24,6 +24,6 @@ sylow.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/solvable/abelian.v b/mathcomp/solvable/abelian.v
index ba26ab6..2163b7d 100644
--- a/mathcomp/solvable/abelian.v
+++ b/mathcomp/solvable/abelian.v
@@ -299,7 +299,7 @@ rewrite partn_dvd ?exponentS ?exponent_gt0 //=; apply/dvdn_partP=> // p.
 rewrite pi_of_part ?exponent_gt0 // => /andP[_ /= pi_p].
 have sppi: {subset (p : nat_pred) <= pi} by move=> q /eqnP->.
 have [P sylP] := Sylow_exists p H; have sPH := pHall_sub sylP.
-have{sylP} sylP: p.-Sylow(G) P.
+have{} sylP: p.-Sylow(G) P.
   rewrite pHallE (subset_trans sPH) //= (card_Hall sylP) eqn_dvd andbC.
   by rewrite -{1}(partn_part _ sppi) !partn_dvd ?cardSg ?cardG_gt0.
 rewrite partn_part ?partn_biglcm //.
diff --git a/mathcomp/solvable/alt.v b/mathcomp/solvable/alt.v
index e67a0f9..f95069a 100644
--- a/mathcomp/solvable/alt.v
+++ b/mathcomp/solvable/alt.v
@@ -270,7 +270,7 @@ have nSyl5: #|'Syl_5(H)| = 1%N.
   move: (dvdn_leq  (isT: (0 < 20)%N) Hdiv).
   by move: (n) Hdiv; do 20 (case=> //).
 case: (Sylow_exists 5 H) => S; case/pHallP=> sSH oS.
-have{oS} oS: #|S| = 5 by rewrite oS p_part Hcard20.
+have{} oS: #|S| = 5 by rewrite oS p_part Hcard20.
 suff: 20 %| #|S| by rewrite oS.
 apply: FF => [|S1]; last by rewrite S1 cards1 in oS.
 apply: char_normal_trans Hnorm; apply: lone_subgroup_char => // Q sQH isoQS.
diff --git a/mathcomp/solvable/extraspecial.v b/mathcomp/solvable/extraspecial.v
index 2dcb1d5..6d1a01f 100644
--- a/mathcomp/solvable/extraspecial.v
+++ b/mathcomp/solvable/extraspecial.v
@@ -538,7 +538,7 @@ elim: Es {+}G => [|E Es IHs] S in n oG expG p3Es defG *.
   by rewrite isog_cyclic_card prime_cyclic ?oZ ?card_pX1p2n //=.
 rewrite big_cons -cprodA in defG; rewrite /= -andbA in p3Es.
 have [[_ T _ defT] defET cTE] := cprodP defG; rewrite defT in defET cTE defG.
-case/and3P: p3Es; move/eqP=> oE; move/eqP=> defZE; move/IHs=> {IHs}IHs.
+move: p3Es => /and3P[/eqP oE /eqP defZE /IHs{}IHs].
 have not_cEE: ~~ abelian E.
   by apply: contra not_le_p3_p => cEE; rewrite -oE -oZ -defZE (center_idP _).
 have sES: E \subset S by rewrite -defET mulG_subl.
diff --git a/mathcomp/solvable/extremal.v b/mathcomp/solvable/extremal.v
index a0c40ee..8e6e002 100644
--- a/mathcomp/solvable/extremal.v
+++ b/mathcomp/solvable/extremal.v
@@ -862,7 +862,7 @@ Proof.
 move=> n_gt1; have [def2q _ ltqm _] := def2qr n_gt1.
 case/(isoGrpP _ (Grp_2dihedral n_gt1)); rewrite card_2dihedral // -/ m => oG.
 case/existsP=> -[x y] /=; rewrite -/q => /eqP[defG xq y2 xy].
-have{defG} defG: <[x]> * <[y]> = G.
+have{} defG: <[x]> * <[y]> = G.
   by rewrite -norm_joinEr // norms_cycle xy groupV cycle_id.
 have notXy: y \notin <[x]>.
   apply: contraL ltqm => Xy; rewrite -leqNgt -oG -defG mulGSid ?cycle_subG //.
@@ -884,7 +884,7 @@ move=> n_gt3; have [def2q _ ltqm _] := def2qr (ltnW (ltnW n_gt3)).
 case/(isoGrpP _ (Grp_semidihedral n_gt3)).
 rewrite card_semidihedral // -/m => oG.
 case/existsP=> -[x y] /=; rewrite -/q -/r => /eqP[defG xq y2 xy].
-have{defG} defG: <[x]> * <[y]> = G.
+have{} defG: <[x]> * <[y]> = G.
   by rewrite -norm_joinEr // norms_cycle xy mem_cycle.
 have notXy: y \notin <[x]>.
   apply: contraL ltqm => Xy; rewrite -leqNgt -oG -defG mulGSid ?cycle_subG //.
@@ -905,7 +905,7 @@ Proof.
 move=> n_gt2; have [def2q def2r ltqm _] := def2qr (ltnW n_gt2).
 case/(isoGrpP _ (Grp_quaternion n_gt2)); rewrite card_quaternion // -/m => oG.
 case/existsP=> -[x y] /=; rewrite -/q -/r => /eqP[defG xq y2 xy].
-have{defG} defG: <[x]> * <[y]> = G.
+have{} defG: <[x]> * <[y]> = G.
   by rewrite -norm_joinEr // norms_cycle xy groupV cycle_id.
 have notXy: y \notin <[x]>.
   apply: contraL ltqm => Xy; rewrite -leqNgt -oG -defG mulGSid ?cycle_subG //.
@@ -1949,7 +1949,7 @@ have [a [fGa oa au n_gt01 cycGs]]: exists a,
   rewrite -(injm_p_rank injf) // p_rank_abelian 1?morphim_abelian //= p2 -/Gs.
   case: leqP => [|fGs1_gt1]; [by left | right].
   split=> //; exists c; last by rewrite -def_m // m_c expg_zneg.
-  have{defA1} defA1: <[a]> \x <[c]> = 'Ohm_1(Aut U).
+  have{} defA1: <[a]> \x <[c]> = 'Ohm_1(Aut U).
     by rewrite -(Ohm_dprod 1 defA) defA1 (@Ohm_p_cycle 1 _ 2) /p_elt oc.
   have def_fGs1: 'Ohm_1(f @* Gs) = 'Ohm_1(A).
     apply/eqP; rewrite eqEcard OhmS // -(dprod_card defA1) -!orderE oa oc.
@@ -2240,7 +2240,7 @@ have tiER: E :&: R = 'Z(E) by rewrite setIA (setIidPl (subset_trans sEH sHG)).
 have [cRR | not_cRR] := boolP (abelian R).
   exists E; [by right | exists [group of R]; split=> //; left].
   by rewrite /= -(setIidPl (sub_abelian_cent cRR sUR)) scUR.
-have{scUR} scUR: [group of U] \in 'SCN(R).
+have{} scUR: [group of U] \in 'SCN(R).
   by apply/SCN_P; rewrite (normalS sUR (subsetIl _ _)) // char_normal.
 have pR: p.-group R := pgroupS (subsetIl _ _) pG.
 have [R_le_3 | R_gt_3] := leqP (logn p #|R|) 3.
diff --git a/mathcomp/solvable/maximal.v b/mathcomp/solvable/maximal.v
index af0001c..7f36723 100644
--- a/mathcomp/solvable/maximal.v
+++ b/mathcomp/solvable/maximal.v
@@ -1216,8 +1216,8 @@ set T := S; exists (logn p #|T|)./2.
 have [Es] := extraspecial_structure pS esS; rewrite -[in RHS]/T.
 elim: Es T => [_ _ <-| E s IHs T] /=.
   by rewrite big_nil cprod1g oZ (pfactorK 1).
-rewrite -andbA big_cons -cprodA; case/and3P; move/eqP=> oEp3; move/eqP=> defZE.
-move/IHs=> {IHs}IHs; case/cprodP=> [[_ U _ defU]]; rewrite defU => defT cEU.
+rewrite -andbA big_cons -cprodA => /and3P[/eqP oEp3 /eqP defZE].
+move=> /IHs{}IHs /cprodP[[_ U _ defU]]; rewrite defU => defT cEU.
 rewrite -(mulnK #|T| (cardG_gt0 (E :&: U))) -defT -mul_cardG /=.
 have ->: E :&: U = 'Z(S).
   apply/eqP; rewrite eqEsubset subsetI -{1 2}defZE subsetIl setIS //=.
@@ -1385,7 +1385,7 @@ have{CAx GAx}: <[coset A x]> <| G / A.
   by rewrite /normal cycle_subG GAx cents_norm // centsC cycle_subG.
 case/(inv_quotientN nsAG)=> B /= defB sAB nBG.
 rewrite -cycle_subG defB (maxA B) ?trivg_quotient // nBG.
-have{defB} defB : B :=: A * <[x]>.
+have{} defB : B :=: A * <[x]>.
   rewrite -quotientK ?cycle_subG ?quotient_cycle // defB quotientGK //.
   exact: normalS (normal_sub nBG) nsAG.
 apply/setIidPl; rewrite ?defB -[_ :&: _]center_prod //=.
diff --git a/mathcomp/solvable/nilpotent.v b/mathcomp/solvable/nilpotent.v
index 06f3152..cf6503a 100644
--- a/mathcomp/solvable/nilpotent.v
+++ b/mathcomp/solvable/nilpotent.v
@@ -424,7 +424,7 @@ have <-: 'Z(H / Z) * 'Z(K / Z) = 'Z(G / Z).
   by rewrite -mulHK quotientMl // center_prod ?quotient_cents.
 have ZquoZ (B A : {group gT}):
   B \subset 'C(A) -> 'Z_n(A) * 'Z_n(B) = Z -> 'Z(A / Z) = 'Z_n.+1(A) / Z.
-- move=> cAB {defZ}defZ; have cAZnB: 'Z_n(B) \subset 'C(A) := gFsub_trans _ cAB.
+- move=> cAB {}defZ; have cAZnB: 'Z_n(B) \subset 'C(A) := gFsub_trans _ cAB.
   have /second_isom[/=]: A \subset 'N(Z).
     by rewrite -defZ normsM ?gFnorm ?cents_norm // centsC.
   suffices ->: Z :&: A = 'Z_n(A).
diff --git a/mathcomp/solvable/primitive_action.v b/mathcomp/solvable/primitive_action.v
index 80005a4..27c0780 100644
--- a/mathcomp/solvable/primitive_action.v
+++ b/mathcomp/solvable/primitive_action.v
@@ -120,7 +120,7 @@ have [trG _] := andP primG; have [x Sx defS] := imsetP trG.
 move: primG; rewrite (trans_prim_astab Sx) // => /maximal_eqP[_].
 case/(_ ('C_G[x | to] <*> H)%G) => /= [||cxH|]; first exact: joing_subl.
 - by rewrite join_subG subsetIl.
-- have{cxH} cxH: H \subset 'C_G[x | to] by rewrite -cxH joing_subr.
+- have{} cxH: H \subset 'C_G[x | to] by rewrite -cxH joing_subr.
   rewrite subsetI sHG /= in cxH; left; apply/subsetP=> a Ha.
   apply/astabP=> y Sy; have [b Gb ->] := atransP2 trG Sx Sy.
   rewrite actCJV [to x (a ^ _)](astab1P _) ?(subsetP cxH) //.
diff --git a/mathcomp/solvable/sylow.v b/mathcomp/solvable/sylow.v
index fcbe7e8..3d2685b 100644
--- a/mathcomp/solvable/sylow.v
+++ b/mathcomp/solvable/sylow.v
@@ -148,7 +148,7 @@ have sylP: p.-Sylow(G) P.
   by rewrite p'natE // -indexgI -oSiN // /dvdn oS1.
 have eqS Q: maxp G Q = p.-Sylow(G) Q.
   apply/idP/idP=> [S_Q|]; last exact: Hall_max.
-  have{S_Q} S_Q: Q \in S by rewrite inE.
+  have{} S_Q: Q \in S by rewrite inE.
   rewrite pHallE -(card_Hall sylP); case: (S_pG Q) => // -> _ /=.
   by case: (atransP2 trS S_P S_Q) => x _ ->; rewrite cardJg.
 have ->: 'Syl_p(G) = S by apply/setP=> Q; rewrite 2!inE.
@@ -568,7 +568,7 @@ Theorem Baer_Suzuki x G :
   x \in 'O_p(G).
 Proof.
 have [n] := ubnP #|G|; elim: n G x => // n IHn G x /ltnSE-leGn Gx pE.
-set E := x ^: G; have{pE} pE: {in E &, forall x1 x2, p.-group <<[set x1; x2]>>}.
+set E := x ^: G; have{} pE: {in E &, forall x1 x2, p.-group <<[set x1; x2]>>}.
   move=> _ _ /imsetP[y1 Gy1 ->] /imsetP[y2 Gy2 ->].
   rewrite -(mulgKV y1 y2) conjgM -2!conjg_set1 -conjUg genJ pgroupJ.
   by rewrite pE // groupMl ?groupV.