Merge pull request #658 from CohenCyril/duplicate_clear

Removing duplicate clears and turning the warning into an error

9 files changed, 16 insertions, 16 deletions

diff --git a/mathcomp/ssreflect/Make b/mathcomp/ssreflect/Make
index d6879a6..b909046 100644
--- a/mathcomp/ssreflect/Make
+++ b/mathcomp/ssreflect/Make
@@ -28,7 +28,7 @@ order.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
 -arg -w -arg -non-reversible-notation
\ No newline at end of file
diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v
index cd3507a..7d8332c 100644
--- a/mathcomp/ssreflect/bigop.v
+++ b/mathcomp/ssreflect/bigop.v
@@ -1770,7 +1770,7 @@ rewrite -{P mem_r}big_r; elim: r Ur => /= [_ | i r IHr].
   rewrite (big_pred1 [ffun=> j0]) ?big_nil //= => f.
   apply/familyP/eqP=> /= [Df |->{f} i]; last by rewrite ffunE !inE.
   by apply/ffunP=> i; rewrite ffunE; apply/eqP/Df.
-case/andP=> /negbTE nri; rewrite big_cons big_distrl => {IHr}/IHr <-.
+case/andP=> /negbTE nri; rewrite big_cons big_distrl => {}/IHr<-.
 rewrite (partition_big (fun f : fIJ => f i) (Q i)) => [|f]; last first.
   by move/familyP/(_ i); rewrite /= inE /= eqxx.
 pose seti j (f : fIJ) := [ffun k => if k == i then j else f k].
diff --git a/mathcomp/ssreflect/div.v b/mathcomp/ssreflect/div.v
index 4899ee3..ae46cd3 100644
--- a/mathcomp/ssreflect/div.v
+++ b/mathcomp/ssreflect/div.v
@@ -709,7 +709,7 @@ rewrite !natTrecE; set m := _ + r; set km := _ + kn; pose d := gcdn m n.
 have ->: gcdn n r = d by rewrite [d]gcdnC gcdnMDl.
 have m_gt0: 0 < m by rewrite addn_gt0 r_gt0 orbT.
 have d_gt0: 0 < d by rewrite gcdn_gt0 m_gt0.
-move/IHq=> {IHq} IHq le_kn_r le_kr_n def_d; apply: IHq => //; rewrite -/d.
+move=> {}/IHq IHq le_kn_r le_kr_n def_d; apply: IHq => //; rewrite -/d.
   by rewrite mulnDl leq_add // -mulnA leq_mul2l le_kr_n orbT.
 apply: (@addIn d); rewrite mulnDr -addnA addnACA -def_d addnACA mulnA.
 rewrite -!mulnDl -mulnDr -addnA [kr * _]mulnC; congr addn.
diff --git a/mathcomp/ssreflect/finfun.v b/mathcomp/ssreflect/finfun.v
index 0218f6a..1fd1a83 100644
--- a/mathcomp/ssreflect/finfun.v
+++ b/mathcomp/ssreflect/finfun.v
@@ -175,7 +175,7 @@ Proof.
 suffices ffunK f g: (forall x, f x = g x) -> f = finfun g.
   by split=> [/ffunK|] -> //; apply/esym/ffunK.
 case: f => f Dg; rewrite unlock; congr FinfunOf.
-have{Dg} Dg x (aTx : mem_seq (enum aT) x): g x = fun_of_fin_rec f aTx.
+have{} Dg x (aTx : mem_seq (enum aT) x): g x = fun_of_fin_rec f aTx.
   by rewrite -Dg /= (bool_irrelevance (mem_enum _ _) aTx).
 elim: (enum aT) / f (enum_uniq aT) => //= x1 s y f IHf /andP[s'x1 Us] in Dg *.
 rewrite Dg ?eqxx //=; case: eqP => // /eq_axiomK-> /= _.
diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v
index 3e60c2d..ef47cd2 100644
--- a/mathcomp/ssreflect/finset.v
+++ b/mathcomp/ssreflect/finset.v
@@ -1840,7 +1840,7 @@ Proof.
 have->: P = [set x in enum (mem P)] by apply/setP=> x; rewrite inE mem_enum.
 elim: {P}(enum _) (enum_uniq (mem P)) => [_ | A e IHe] /=.
   by rewrite /trivIset /cover !big_set0 cards0; left=> A; rewrite inE.
-case/andP; rewrite set_cons -(in_set (fun B => B \in e)) => PA {IHe}/IHe.
+case/andP; rewrite set_cons -(in_set (fun B => B \in e)) => PA {}/IHe.
 move: {e}[set x in e] PA => P PA IHP.
 rewrite /trivIset /cover !big_setU1 //= eq_sym.
 have:= leq_card_cover P; rewrite -(mono_leqif (leq_add2l #|A|)).
@@ -2157,7 +2157,7 @@ move=> /and3P[/eqP defG tiP notP0] /and3P[/eqP defP tiQ notQ0].
 have sQP E: E \in Q -> {subset E <= P}.
   by move=> Q_E; apply/subsetP; rewrite -defP (bigcup_max E).
 rewrite /partition cover_imset -(big_trivIset _ tiQ) defP -defG eqxx /= andbC.
-have{notQ0} notQ0: set0 \notin cover @: Q.
+have{} notQ0: set0 \notin cover @: Q.
   apply: contra notP0 => /imsetP[E Q_E E0].
   have /set0Pn[/= A E_A] := memPn notQ0 E Q_E.
   congr (_ \in P): (sQP E Q_E A E_A).
diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v
index f40c1d5..97e34a2 100644
--- a/mathcomp/ssreflect/order.v
+++ b/mathcomp/ssreflect/order.v
@@ -6965,7 +6965,7 @@ Lemma leEtprod n T (t1 t2 : n.-tuple T) :
 Proof.
 elim: n => [|n IHn] in t1 t2 *.
   by rewrite tuple0 [t2]tuple0/= lexx; symmetry; apply/forallP => [].
-case: (tupleP t1) (tupleP t2) => [x1 {t1}t1] [x2 {t2}t2].
+case: (tupleP t1) (tupleP t2) => [x1 {}t1] [x2 {}t2].
 rewrite [_ <= _]le_cons [t1 <= t2 :> seq _]IHn.
 apply/idP/forallP => [/andP[lex12 /forallP/= let12 i]|lext12].
   by case: (unliftP ord0 i) => [j ->|->]//; rewrite !tnthS.
@@ -7275,7 +7275,7 @@ Lemma lexi_tupleP n T (t1 t2 : n.-tuple T) :
 Proof.
 elim: n => [|n IHn] in t1 t2 *.
   by rewrite tuple0 [t2]tuple0/= lexx; constructor; exists ord0 => -[].
-case: (tupleP t1) (tupleP t2) => [x1 {t1}t1] [x2 {t2}t2].
+case: (tupleP t1) (tupleP t2) => [x1 {}t1] [x2 {}t2].
 rewrite [_ <= _]lexi_cons; apply: (iffP idP) => [|[k leif_xt12]].
   case: comparableP => //= [ltx12 _|-> /IHn[k kP]].
     exists ord0 => i; rewrite leqn0 => /eqP/(@ord_inj n.+1 i ord0)->.
@@ -7296,7 +7296,7 @@ Lemma ltxi_tupleP n T (t1 t2 : n.-tuple T) :
 Proof.
 elim: n => [|n IHn] in t1 t2 *.
   by rewrite tuple0 [t2]tuple0/= ltxx; constructor => - [] [].
-case: (tupleP t1) (tupleP t2) => [x1 {t1}t1] [x2 {t2}t2].
+case: (tupleP t1) (tupleP t2) => [x1 {}t1] [x2 {}t2].
 rewrite [_ < _]ltxi_cons; apply: (iffP idP) => [|[k leif_xt12]].
   case: (comparableP x1 x2) => //= [ltx12 _|-> /IHn[k kP]].
     exists ord0 => i; rewrite leqn0 => /eqP/(@ord_inj n.+1 i ord0)->.
diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v
index 72c9719..fa66807 100644
--- a/mathcomp/ssreflect/path.v
+++ b/mathcomp/ssreflect/path.v
@@ -687,12 +687,12 @@ Proof.
 move=> e_p; have: x \in x :: p by apply: mem_head.
 elim: p x {1 3 5}x e_p => [|y2 p IHp] x y1.
   by rewrite mem_seq1 => _ /eqP->.
-rewrite inE orbC /= => /andP[ey12 /IHp {IHp}IHp].
+rewrite inE orbC /= => /andP[ey12 {}/IHp IHp].
 case: ifPn => [y2p_x _ | not_y2p_x /eqP def_x].
   have [p' e_p' Up' p'p] := IHp _ y2p_x.
   by split=> // y /p'p; apply: predU1r.
 have [p' e_p' Up' p'p] := IHp y2 (mem_head y2 p).
-have{p'p} p'p z: z \in y2 :: p' -> z \in y2 :: p.
+have{} p'p z: z \in y2 :: p' -> z \in y2 :: p.
   by rewrite !inE; case: (z == y2) => // /p'p.
 rewrite -(last_cons y1) def_x; split=> //=; first by rewrite ey12.
 by rewrite (contra (p'p y1)) -?def_x.
diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v
index 389b1c2..ab8edce 100644
--- a/mathcomp/ssreflect/prime.v
+++ b/mathcomp/ssreflect/prime.v
@@ -216,13 +216,13 @@ have eq_bc_0: (b == 0) && (c == 0) = (d == 0).
 have lt1p: 1 < p by rewrite ltnS double_gt0.
 have co_p_2: coprime p 2 by rewrite /coprime gcdnC gcdnE modn2 /= odd_double.
 have if_d0: d = 0 -> [/\ m = (p + a.*2) * p, lb_dvd p p & lb_dvd p (p + a.*2)].
-  move=> d0; have{d0 def_m} def_m: m = (p + a.*2) * p.
+  move=> d0; have{d0} def_m: m = (p + a.*2) * p.
     by rewrite d0 addn0 -!mul2n mulnA -mulnDl in def_m *.
   split=> //; apply/hasPn=> r /(hasPn leppm); apply: contra => /= dv_r.
     by rewrite def_m dvdn_mull.
   by rewrite def_m dvdn_mulr.
 case def_a: a => [|a'] /= in le_a_n *; rewrite !natTrecE -/p {}eq_bc_0.
-  case: d if_d0 def_m => [[//| def_m {pr_p}pr_p pr_m'] _ | d _ def_m] /=.
+  case: d if_d0 def_m => [[//| def_m {}pr_p pr_m'] _ | d _ def_m] /=.
     rewrite def_m def_a addn0 mulnA -2!expnSr.
     by split; rewrite /pd_ord /pf_ok /= ?muln1 ?pr_p ?leqnn.
   apply: apd_ok; rewrite // /pd_ok /= /pfactor expn1 muln1 /pd_ord /= ltpm.
@@ -256,11 +256,11 @@ have ltdp: d < p.
   move/eqP: def_b'; rewrite subn_eq0 -(@leq_pmul2r kb); last first.
     by rewrite -def_kb1.
   rewrite mulnBl -def_k2 ltnS -(leq_add2r c); move/leq_trans; apply.
-  have{ltc} ltc: c < k.*2.
+  have{} ltc: c < k.*2.
     by apply: (leq_trans ltc); rewrite leq_double /kb; case e.
   rewrite -{2}(subnK (ltnW ltc)) leq_add2r leq_sub2l //.
   by rewrite -def_kb1 mulnS leq_addr.
-case def_d: d if_d0 => [|d'] => [[//|{def_m ltdp pr_p} def_m pr_p pr_m'] | _].
+case def_d: d if_d0 => [|d'] => [[//|{ltdp pr_p}def_m pr_p pr_m'] | _].
   rewrite eqxx -doubleS -addnS -def_a doubleD -addSn -/p def_m.
   rewrite mulnCA mulnC -expnSr.
   apply: IHn => {n le_a_n}//; rewrite -/p -/kb; split.
diff --git a/mathcomp/ssreflect/tuple.v b/mathcomp/ssreflect/tuple.v
index db53235..f32793f 100644
--- a/mathcomp/ssreflect/tuple.v
+++ b/mathcomp/ssreflect/tuple.v
@@ -349,7 +349,7 @@ Proof.
 case=> /= t t_n; rewrite -(count_map _ (pred1 t)) (pmap_filter (insubK _)).
 rewrite count_filter -(@eq_count _ (pred1 t)) => [|s /=]; last first.
   by rewrite isSome_insub; case: eqP=> // ->.
-elim: n t t_n => [|m IHm] [|x t] //= {IHm}/IHm; move: (iter m _ _) => em IHm.
+elim: n t t_n => [|m IHm] [|x t] //= {}/IHm; move: (iter m _ _) => em IHm.
 transitivity (x \in T : nat); rewrite // -mem_enum codomE.
 elim: (fintype.enum T) (enum_uniq T) => //= y e IHe /andP[/negPf ney].
 rewrite count_cat count_map inE /preim /= [in LHS]/eq_op /= eq_sym => /IHe->.