Removing duplicate clears and turning the warning into an error

4 files changed, 6 insertions, 6 deletions

diff --git a/mathcomp/fingroup/Make b/mathcomp/fingroup/Make
index a765cd3..0f25f14 100644
--- a/mathcomp/fingroup/Make
+++ b/mathcomp/fingroup/Make
@@ -13,6 +13,6 @@ quotient.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/fingroup/automorphism.v b/mathcomp/fingroup/automorphism.v
index b9ed8e1..a2cda05 100644
--- a/mathcomp/fingroup/automorphism.v
+++ b/mathcomp/fingroup/automorphism.v
@@ -432,7 +432,7 @@ Lemma lone_subgroup_char G H :
   H \char G.
 Proof.
 move=> sHG Huniq; apply/charP; split=> // f injf Gf; apply/eqP.
-have{injf} injf: {in H &, injective f}.
+have{} injf: {in H &, injective f}.
   by move/injmP: injf; apply: sub_in2; apply/subsetP.
 have fH: f @* H = f @: H by rewrite /morphim (setIidPr sHG).
 rewrite eqEcard {2}fH card_in_imset ?{}Huniq //=.
diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v
index 21e1e49..914c332 100644
--- a/mathcomp/fingroup/fingroup.v
+++ b/mathcomp/fingroup/fingroup.v
@@ -866,7 +866,7 @@ suffices{big_r} IHr: reflect (exists2 c, inA c r & x = \prod_(i <- r) c i) piAx.
   apply: (iffP IHr) => -[c inAc ->]; do [exists c; last by rewrite big_r].
     by move=> i Pi; rewrite (allP inAc) ?mem_r.
   by apply/allP=> i; rewrite mem_r => /inAc.
-elim: {P mem_r}r x @piAx Ur => /= [x _ | i r IHr x /andP[r'i /IHr{IHr}IHr]].
+elim: {P mem_r}r x @piAx Ur => /= [x _ | i r IHr x /andP[r'i /IHr{}IHr]].
   by rewrite unlock; apply: (iffP set1P) => [-> | [] //]; exists (fun=> x).
 rewrite big_cons; apply: (iffP idP) => [|[c /andP[Aci Ac] ->]]; last first.
   by rewrite big_cons mem_mulg //; apply/IHr=> //; exists c.
diff --git a/mathcomp/fingroup/gproduct.v b/mathcomp/fingroup/gproduct.v
index cdd68fd..47f9353 100644
--- a/mathcomp/fingroup/gproduct.v
+++ b/mathcomp/fingroup/gproduct.v
@@ -393,7 +393,7 @@ have [/= f inj_f im_f] := third_isom (joing_subl K M) nsKG nsKMG.
 rewrite quotientYidl //= -imKH -(restrm_quotientE nKH sMH) in f inj_f im_f.
 have /domP[h [_ ker_h _ im_h]]: 'dom (f \o quotm _ nsMH) = H / M.
   by rewrite ['dom _]morphpre_quotm injmK.
-have{im_h} im_h L: L \subset H -> h @* (L / M) = K <*> L / (K <*> M).
+have{} im_h L: L \subset H -> h @* (L / M) = K <*> L / (K <*> M).
   move=> sLH; have [sLG sKKM] := (subset_trans sLH sHG, joing_subl K M).
   rewrite im_h morphim_comp morphim_quotm [_ @* L]restrm_quotientE ?im_f //.
   rewrite quotientY ?(normsG sKKM) ?(subset_trans sLG) ?normal_norm //.
@@ -811,7 +811,7 @@ Proof.
 elim: r G => [|i r IHr]; rewrite !(big_nil, big_cons) //; case: ifP => _ // G.
 case/cprodP=> [[K H -> defH]]; rewrite defH => <- cKH leKH_G.
 have /implyP := leq_trans leKH_G (dvdn_leq _ (dvdn_cardMg K H)).
-rewrite muln_gt0 leq_pmul2l !cardG_gt0 //= => /(IHr H defH){defH}defH.
+rewrite muln_gt0 leq_pmul2l !cardG_gt0 //= => /(IHr H defH){}defH.
 by rewrite defH dprodE // cardMg_TI // -(bigdprod_card defH).
 Qed.
 
@@ -825,7 +825,7 @@ have [m leQm] := ubnP #|Q|; elim: m => // m IHm in (Q) leQm G defG sQP *.
 have [i Qi | Q0] := pickP Q; last by rewrite !big_pred0 in defG *.
 move: defG; rewrite !(bigD1 i Qi) /= => /cprodP[[Hi Gi defAi defGi] <-].
 rewrite defAi defGi => cHGi.
-have{defGi} defGi: \big[dprod/1]_(j | Q j && (j != i)) A j = Gi.
+have{} defGi: \big[dprod/1]_(j | Q j && (j != i)) A j = Gi.
   by apply: IHm => [||j /andP[/sQP]] //; rewrite (cardD1x Qi) in leQm.
 rewrite defGi dprodE // coprime_TIg // -defAi -(bigdprod_card defGi).
 elim/big_rec: _ => [|j n /andP[neq_ji Qj] IHn]; first exact: coprimen1.