[WIP]removed deprecation warnings and most duplicate clear warnings

theories/approx.v

@@ -98,7 +98,7 @@ Proof. by apply/(@intR_leP R 1); rewrite lez_nat expn_gt0. Qed.
 Lemma ltR0exp2 s : 0 < exp2R s.
 Proof. exact/(ltR_le_trans ltR01)/leR1exp2. Qed.
 Arguments ltR0exp2 : clear implicits.
-Hint Resolve ltR0exp2.
+Hint Resolve ltR0exp2 : core.
 
 Lemma exp2R_add s1 s2 : exp2R (s1 + s2) == exp2R s1 * exp2R s2.
 Proof. by rewrite /exp2R expnD -intRM. Qed.

theories/birkhoff.v

@@ -314,7 +314,7 @@ apply: (@colorable_from_ring _ geoG planarG _ Ur1 _ nt_r1 (e :: et)).
     suffices ->: e :: et = ctrace (belast e et).
       by rewrite -[ctrace _](mapK (inv_permc g)); apply: tr1_et.
     by rewrite -Dct0 /= (scanlK addKc).
-  case: Kempe_tree_closure => ctu3 [[] // gtu3] {tr1'et r1valid}r1valid _.
+  case: Kempe_tree_closure => ctu3 [[] // gtu3] {tr1'et}{}r1valid _.
   case/orP=> [/(chkbP r1)[]// et1 tr_et1 ct3'et1 | {r1closed}/idPn[]].
     suffices sz_et1: size et1 = n'.+1.
       by have[] := Kempe_validP r1valid sz_et1 ct3'et1 r1closed tr_et1.
@@ -336,7 +336,7 @@ have []:= @Kempe_tree_closure_correct n' (P r2 Ur2) n ctu2 ctr gtu2.
     by rewrite rev_cons rev_rcons /= addc_eq0 => /eqP->.
   rewrite -rot1_cons -Dct0 -[rev _](rotrK 1) -rev_rot -!trace_rot -trace_rev.
   exact: sumt_trace.
-case: Kempe_tree_closure => ctu3 [[] // gtu3] {r2valid tr2'et}r2valid _.
+case: Kempe_tree_closure => ctu3 [[] // gtu3] {tr2'et}{}r2valid _.
 case/orP=> [/(chkbP r2)[]// et3 tr_et3 ct'et3 | /idPn[]]; last exact: (IHnm r1).
 suffices sz_et3: size et3 = n'.+1.
   by have [] := Kempe_validP r2valid sz_et3 ct'et3 r2closed tr_et3.

theories/cfcolor.v

@@ -380,7 +380,7 @@ have:= De12; rewrite [e1]addcC => /addcI KnG.
 have k'F: invariant face k' =1 ecpA G2.
   move=> x; apply/eqP; move: (fconnect1 face x); rewrite cface_icpA /k'.
   case/orP=> [/fconnect_invariant <-// | /allP kFx].
-  have{kFx} kFx y: y \in [:: x; face x] -> k y = k (node G2).
+  have{} kFx y: y \in [:: x; face x] -> k y = k (node G2).
     move/kFx; rewrite /= unfold_in => /hasP[z Dz /fconnect_invariant-> //].
     by move: Dz; rewrite !inE => /pred2P[]->.
   by rewrite /= kFx ?(kFx x) // ?inE ?eqxx ?orbT.

theories/cfcontract.v

@@ -104,7 +104,7 @@ elim: cp => //=; case=> // [n||] cp IHcp.
   rewrite cpring_ecpR /rot !insertE_cat -catA uniq_catCA catA /=.
   by rewrite -insertE_cat cat_take_drop.
 - rewrite cpring_ecpY; case Dcp: cp => [|s cp']; first by rewrite cpring0.
-  rewrite -{s cp'}Dcp; set G := cpmap cp => /IHcp{IHcp} IHcp.
+  rewrite -{s cp'}Dcp; set G := cpmap cp => /IHcp {}IHcp.
   rewrite 2!cat_cons (insertE_cat [:: _; _]) -map_cons -map_cat.
   rewrite insertE_icpY cat_uniq has_map has_pred0 !andTb.
   rewrite (map_inj_uniq (@icpY_inj G G)) -cat1s !insertE_cat uniq_catCA.
@@ -732,7 +732,7 @@ case: s Dcpc => // [n||] Dcpc; rewrite !implyTb => cp_ok Emr Emc;
     by case: b1 b2 b3 => [] [] [].
   rewrite -Dcp -/G; have plainGX: plain (ecpY G) := plain_ecpY G plainG.
   case: ifP => // b123; rewrite [size _]/= [size _ = _]/= => [] [Emc] [Emr].
-  case: (cfctr _ _)  {IHcp}(IHcp (b3 :: mr) mc Emr Emc) => // {cpc} cpc IHcp _.
+  case: (cfctr _ _)  {IHcp}(IHcp (b3 :: mr) mc Emr Emc) => // {}cpc IHcp _.
   have <-: map (icpY G) (node G :: ctrenum cp) = ctrenum (CpY :: cp).
     by rewrite /G Dcp.
   move: IHcp; set p := _ ++ _; rewrite sparse_cons -(eq_has (mem_cpring G)).
@@ -764,7 +764,7 @@ case: s Dcpc => // [n||] Dcpc; rewrite !implyTb => cp_ok Emr Emc;
 case: mc mr Emc Emr Dcpc => [|b3 [|b4 [|b5 mc]]] [|b1 [|b2 mr]] // [Emc] Emr.
 rewrite /= in Emc Emr; case: ifP => // b314_325; case: ifP => // _.
 have{IHcp}:= IHcp [:: b4, b5 & mr] mc Emr Emc; set p := _ ++ _.
-case: (cfctr _ _ _) => // []{cpc} cpc IHcp _; rewrite {cpc}implyTb in IHcp.
+case: (cfctr _ _ _) => // []{}cpc IHcp _; rewrite {cpc}implyTb in IHcp.
 have plainGX := plain_ecpH G plainG.
 have <-: face (ecpH G) :: map (icpH G) [:: node G, G : G & ctrenum cp] =
           ctrenum (CpH :: cp) by [].
@@ -988,7 +988,7 @@ apply/andP; split=> [{mtc_max} | {mtc_min}]; last first.
     by case/hasP=> z /ccAx xAz /adjFr->.
   move: mc mt Emcq Emtq Uq; rewrite simple_recI.
   elim: q => [|y q IHq] [|b1 m1] // [|b2 m2] //= Em1 Em2 /andP[qF'y Uq].
-  have{qF'y} qF'y m: (y \in fband (mask m q)) = false.
+  have {}qF'y m: (y \in fband (mask m q)) = false.
     by apply: contraNF qF'y; apply: has_mask.
   case: b1 b2 => [] [] //= q12F; try apply: (IHq m1 m2) => //.
   - move=> z q1Fz; have:= q12F z; rewrite !unfold_in /=.
@@ -1017,7 +1017,7 @@ rewrite {n_Ax_cc DccF DmtF}/nF_qtc simple_fcard_fband; last first.
 move: mc mt Emcq Emtq Uq; rewrite simple_recI.
 elim: q => [|y q IHq] [|b1 m1] // [|b2 m2] //= Em1 Em2 /andP[qF'y Uq].
 set q1 := mask m1 q; set q2 := mask m2 q.
-have{qF'y} qF'y m: (y \in fband (mask m q)) = false.
+have{} qF'y m: (y \in fband (mask m q)) = false.
   by apply: contraNF qF'y; apply: has_mask.
 have Eq21: filter (fband (y :: q2)) q1 = filter (fband q2) q1.
   apply: eq_in_filter => z q1z; apply: orb_idl; rewrite cfaceC => yFz.

theories/cfmap.v

@@ -412,7 +412,7 @@ rewrite edgeK /=; case ex0Fnx0: (cface (edge x0) (node x0)).
   by rewrite /ecpA_face ex0Fnx0 -cface1.
 have: cface (node x0) (edge (node (node x0))) by rewrite cface1r nodeK.
 case/connectP=> _ /shortenP[p nx0Fp Up _] Lp.
-have:= nx0Fp; rewrite -(map_path baseF_ecpA) ?map_id => [{nx0Fp}nx0Fp|].
+have:= nx0Fp; rewrite -(map_path baseF_ecpA) ?map_id => [{}nx0Fp|].
   rewrite (@cfaceC ecpA) (connect_trans (path_connect nx0Fp (mem_last _ _))) //.
   apply: connect1; rewrite -Lp /= /ecpA_face ex0Fnx0 nodeK eqxx.
   by rewrite (canF_eq (canF_sym faceK)); case: ifP.
@@ -1474,7 +1474,7 @@ rewrite /cpmask => /cpW; elim: cp cm => [|s cp IHcp] [mr mk] cp_ok /= m_ok u.
   by case: mr mk u m_ok => [|[] [|[] []]] // [] // [].
 rewrite orFb in cp_ok; case: s => // [n||] in u cp_ok m_ok *.
 - set cm := Cfmask _ mk; have [/eqP Emr _] := andP m_ok.
-  have{m_ok} m_ok: proper_cpmask cp cm by rewrite /= size_rotr.
+  have{} m_ok: proper_cpmask cp cm by rewrite /= size_rotr.
   move: (cpadj_proper m_ok) {IHcp}(IHcp cm (cpW cp cp_ok) m_ok).
   case: (cpadj cm cp) => mr' mk' /andP[/eqP Emr' _] IHm.
   rewrite -(size_rotr n) -size_ring_cpmap in Emr.

theories/cfquiz.v

@@ -389,7 +389,7 @@ elim: cp2 => [|s cp2 IHcp] in cp2ok (cp1) cp1ok (qs) * => [[] | rqs_ok qsR].
 have scp2ok: config_prog (s :: cp2) by [].
 have{cp2ok} [cp2ok]: nilp cp2 || config_prog cp2 /\ cubic_prog (s :: cp1).
   by case: (s) cp2ok qsR => //=; case: (cp2).
-move/(IHcp cp2ok) => {IHcp}IHcp; rewrite /= in IHcp; move: IHcp rqs_ok qsR.
+move/(IHcp cp2ok) => {}IHcp; rewrite /= in IHcp; move: IHcp rqs_ok qsR.
 case Dqs: qs => [|rq1 [|rq2 [|rq3 qs3]]] //; rewrite -Dqs.
 set G := cpmap cp2; set r := cpring G; set h := @injcp cp1 _.
 have Ih: injective h by apply: injcp_inj.
@@ -472,7 +472,7 @@ case: s scp2ok (config_prog_cubic scp2ok) => // [n||] cp2ok cp2Q;
   rewrite -hF in nu0FnG; rewrite (arity_cface nu0FnG) !nFiG !fband_cons /=.
   rewrite !connect0 orbT -/r -/r1 !add1n addn2 !addnS => /and5P[].
   set v1 := icpY G (node G) => Ea1 q1nG Ea2 q2nu0 /and3P[Ea3 q3iG q_r1].
-  have{q_r1} q_r1: rqs_fit h1 qs3 r1.
+  have{} q_r1: rqs_fit h1 qs3 r1.
     move Dea: (fun x => arity (icpY G x) == arity x) => ea.
     have ea_r1: all ea r1.
       apply/allP=> x r1x; rewrite -Dea nFiG [_ \in _]negbTE //.
@@ -641,7 +641,7 @@ rewrite map_cons -/v3 !rqs_fit_cons nFu0 (arity_cface nu0Fv1) in q_r.
 rewrite -hF in nu0Fv1; rewrite (arity_cface nu0Fv1) in q_r.
 rewrite !{1}nFiG /= !fband_cons !connect0 !orbT !addnS addn0 in q_r.
 case/and5P: q_r => Ea1 q1nu0 Ea2 q2u0 /and3P[Ea3 q3v3 q_r1].
-have{q_r1} q_r1: rqs_fit h1 qs3 r1.
+have{} q_r1: rqs_fit h1 qs3 r1.
   move Dea: (fun x => arity (icpH G x) == arity x) => ea.
   have: all ea r1.
     apply/allP=> x r1x; rewrite -Dea nFiG // [x \in _]negbTE //=.

theories/cube.v

@@ -177,7 +177,7 @@ suffices{oQ oEQ oNQ oFQ} oGQ: n_comp glink qmap = n_comp glink G.
   rewrite {1}/genus /Euler_lhs /Euler_rhs oQ oEQ oNQ oFQ oGQ.
   by rewrite mulSn 2!addnA -mulnDl addnC subnDl.
 have g1eq y g_y G x := @same_connect1 _ _ (@glinkC G) x (y G x) (g_y G x).
-have{g1eq} g1eq := (g1eq _ glinkE, g1eq _ glinkN, g1eq _ glinkF).
+have{} g1eq := (g1eq _ glinkE, g1eq _ glinkN, g1eq _ glinkF).
 have [[cGG cGQ] [[g1e g1n] g1f]] := (@clinkC G, @clinkC qmap, g1eq).
 rewrite -!(eq_n_comp (@clink_glink _)) (adjunction_n_comp (tsI CTnf) _ cGG) //.
 apply: (intro_adjunction _ _ (fun x _ => tsE x)) => // [u _ | x _].

theories/dedekind.v

@@ -53,6 +53,7 @@ Implicit Types n i : nat.
 
 (* Dedekind cuts. *)
 
+Declare Scope cut_scope.
 Delimit Scope cut_scope with cut.
 Open Scope cut_scope.
 
@@ -116,7 +117,7 @@ Lemma leRR x : x <= x. Proof. by []. Qed.
 Arguments leRR x : clear implicits.
 
 Lemma eqRR x : x == x. Proof. by split. Qed.
-Hint Resolve leRR eqRR.
+Hint Resolve leRR eqRR : core.
 
 Lemma eqR_sym x y : x == y -> y == x. Proof. by case. Qed.
 
@@ -518,7 +519,7 @@ elim/opp_ind: y => [y IHy | y le0y] in z *.
   by apply/eqR_opp2; rewrite oppD -!mulRN oppD IHy.
 without loss le0z: y z le0y / z >= 0.
   move=> IHz; have [/gec0_opp-le0nz | /(IHz y)->//] := ltcP z 0.
-  move Dt: (y + z) => t; have{Dt} Dt: y + z == t by rewrite Dt.
+  move Dt: (y + z) => t; have {} Dt: y + z == t by rewrite Dt.
   elim/opp_ind: t => [t IHt | t le0t] in y z Dt le0y le0nz *.
     by apply/eqR_opp2; rewrite oppD -!mulRN addC -IHt ?oppK // addC -oppD Dt.
   rewrite -(add0 (x * t)) -(addN (x * z)) -mulRN -addA -{}IHz //.

theories/discretize.v

@@ -203,7 +203,7 @@ pose s := \sum_a (ab0 a).1; pose s_ a := \sum_(b | b != a) (ab0 b).1.
 have Ds a: s = s_ a + (ab0 a).1 by rewrite addnC [s](bigD1 a).
 pose ab_ a := refine_srect (s_ a).+1 (ab0 a).
 exists (fun e => if insub e is Some e then (ab_ e).2 else r0).
-have{ar_ab} ar_ab a z: ab_ a z -> ar a z by move/in_refine_srect/ar_ab.
+have {}ar_ab a z: ab_ a z -> ar a z by move/in_refine_srect/ar_ab.
 split=> [e f p | | e [adj_e lte]]; last 1 first.
 - have [a _ _|/negP[]] := insubP; last exact/arcP.
   have [p _ /insetW-ab0a_p] := ab0ap a.
@@ -373,7 +373,7 @@ have{ab_mrP} ab_cmP e i: ab_cm_proper ab cm e i.
     by apply/hasP; exists q; rewrite // -[q](approx_point_inj Dp) ?Ds1.
   have [_ ->//] := ab_mrP e i ab_e; exists (scale_point R s p).
   by split; last apply/m0i_cm; rewrite -Ds1; apply/mem_approx_scale.
-have{cmP} cmP: cm_proper cm.
+have {}cmP: cm_proper cm.
   move=> i j /hasP[p /= cmi_p cmj_p].
   have [_ /(_ j)-> //] := mrP i; apply: m0tr (scale_point R s1 p) _ _ _.
     by have [m0_cmi _] := cmP i; apply/m0_cmi/mem_approx_scale.

theories/embed.v

@@ -1379,7 +1379,7 @@ Proof.
 split; try exact: embed_sparse; rewrite ?disjoint_has // size_map ?mapEh1.
   by have [[]] := Cred_cc.
 have [[rc'cc _ _ triad_cc] _] := Cred_cc; rewrite disjoint_has has_sym in rc'cc.
-move=> {triad_cc}/triad_cc/existsP[x /= /and3P[ac_x adj3x xA'cc]].
+move=> {}/triad_cc/existsP[x /= /and3P[ac_x adj3x xA'cc]].
 apply/existsP; exists (h1 x); apply/and3P; split=> // [{xA'cc} | {adj3x}].
   apply: leq_trans adj3x _; rewrite orbitF_h1 // /orbit.
   move: (arity x) => n; elim: n => //= n IHn in x ac_x *.
@@ -1388,7 +1388,7 @@ apply/existsP; exists (h1 x); apply/and3P; split=> // [{xA'cc} | {adj3x}].
   by case: hasP => // [[]]; exists y => //=; apply: cface_h1.
 apply: contra xA'cc => /subsetP ccAx; apply/subsetP=> y cc_y.
 have cc_ey: edge y \in insertE cc by apply: ccE.
-have{ccAx} ccAx z: z \in insertE cc -> adj (h1 x) (h1 z).
+have {}ccAx z: z \in insertE cc -> adj (h1 x) (h1 z).
   by move=> cc_z; apply/ccAx/map_f.
 have bc_ey: edge y \in bc by apply: (hasPn rc'cc).
 have: cface x (node y) || cface x (node (edge y)).

theories/finitize.v

@@ -157,7 +157,7 @@ exists h => z t; split=> [mzt | [i le_i_n [Dhz Dht]]].
     by exists n; rewrite // /h !IFR_then // -(map_transl mP mzt).
   have [[//| i /leqW-lt_i_n1 Dgzt_i] _] := gP z t; exists i => //.
   by rewrite /h -(map_transl mP mzt) IFR_else 1?IFR_then // IFR_else ?IFR_then.
-generally have m_t, m_z: z Dhz / m z z; last have{m_t} m_t: m t t by apply: m_t.
+generally have m_t, m_z: z Dhz / m z z; last have {}m_t: m t t by apply: m_t.
   have: (h z < n.+1%:R)%Rval by rewrite Dhz Dht; apply/RleqP; rewrite -ltnNge.
   by apply: RcontraR => m'z; rewrite /h !IFR_else // => /(map_cover mP)[].
 generally have m_tnP, m_zn: z Dhz m_z / m z (f n) <-> i == n.

theories/geometry.v

@@ -157,7 +157,7 @@ Proof. exact/iter_order/faceI. Qed.
 
 Lemma iter_face_subn n x :
   n <= arity x -> iter (arity x - n) face (iter n face x) = x.
-Proof. by move=> le_n_x; rewrite -iter_add subnK ?iter_face_arity. Qed.
+Proof. by move=> le_n_x; rewrite -iterD subnK ?iter_face_arity. Qed.
 
 Lemma arity_mirror : @arity (mirror G) =1 @arity G.
 Proof. by move=> x; apply/eq_card/(cface_mirror x). Qed.

theories/grid.v

@@ -176,7 +176,7 @@ Proof. by rewrite -[d1 in LHS]halfgK addrAC -addrA halfg_add2. Qed.
 
 Lemma oddgP d : is_oddg (oddg d).
 Proof. by case: d => x y /=; rewrite !modz2; do 2!case: odd; constructor. Qed.
-Hint Resolve oddgP.
+Hint Resolve oddgP : core.
 
 Lemma oddg_id c : is_oddg c -> oddg c = c. Proof. by case. Qed.
 
@@ -587,5 +587,6 @@ Qed.
 
 End GridGeometry.
 
-Hint Resolve oddgP.
+#[export]
+Hint Resolve oddgP : core.
 Arguments insetP {r p}.

theories/gridmap.v

@@ -574,7 +574,7 @@ have{cycNr kN} k_r i: {in r i &, forall x y, k x = k y}.
 pose kn x := Ordinal (index_size (k x) [:: Color0; Color1; Color2] : _ < 4)%N.
 exists (fun i => oapp kn ord0 [pick x in r i]) => e /ab_cmP/hasP[d].
 rewrite !inE eqE /= -!val_gmring => /mapP[u r2u {d}->] /mapP[eu r1eu Deu].
-have{Deu} Deu: edge u = eu by apply/val_inj.
+have {}Deu: edge u = eu by apply/val_inj.
 rewrite -{eu}Deu -!{}Dr !mem_rev in r2u r1eu.
 case/mapP: r2u r1eu => x r2x ->; rewrite -hE mem_map // => r1ex.
 apply: contraFN (kE x); have [y /= /k_r <- | /(_ (edge x))/idP] // := pickP.

theories/gtreerestrict.v

@@ -271,7 +271,7 @@ pose gm := =^~ (gtr_match0E, gtr_match1E, gtr_match2E, gtr_match3E).
 elim: t => /= [t0 IHt0 t1 IHt1 t2 IHt2 t3 IHt3|||||||||] in r w *;
   case Dr: r => [|bs ct r'];
   do [ by rewrite /= gtree_mem_empty ?andbF | rewrite -{bs ct r'}Dr];
-  try by do 2?case: ifP => /(pair gm){gm}gm; case: w => [|[][]] //; rewrite !gm.
+  try by do 2?case: ifP => /(pair gm){}gm; case: w => [|[][]] //; rewrite !gm.
 rewrite gtr_split_eq gtree_mem0_cons_pairs; try exact: gtree_restrict_partition.
 by case: w => [|s w]; rewrite // (gtr_mem_gsplit r); case: s => /=.
 Qed.

theories/hubcap.v

@@ -214,7 +214,7 @@ case fit_xr: (fitp x r); last by move=> _ /IHm-> //=; rewrite fit_xr.
 set p1 := meet_part p r; have Exp1: exact_fitp x p1 by apply: exact_fitp_meet.
 have [_ fit_xp1] := andP Exp1; rewrite (check_unfitP fit_xp1) //.
 have [dnt] := sort_drulesP fit_xp1 rt; have [dns] := sort_drulesP fit_xp1 rs.
-move=> {rs rt fit_xp1} rs rt bound_p1 _.
+move=> {fit_xp1} {}rs {}rt bound_p1 _.
 case Dnt1: (_ - dnt) => [|nt1] in bound_p1.
   by case/idPn: Exp1; apply: redpP.
 have le_dnt: dnt <= dns + nt by rewrite ltnW // -subn_gt0 Dnt1.
@@ -278,7 +278,7 @@ elim: m rt1 => // m IHm [|r rt1]/= in nt x1 i nFx1 ub_i rs1 ru1 p1 b1ru1 Exp1 *.
   rewrite ![_ + dbound1 _ x2]addnC -[0]/(dbound1 [::] x1).
   move: rs1 ru1 p1 b1ru1 Exp1.
   have <-: iter i1 face x2 = x1.
-    by rewrite -iter_add subnK // -nFx1 iter_face_arity.
+    by rewrite -iterD subnK // -nFx1 iter_face_arity.
   by apply: IHm => //; rewrite ?arity_iter_face ?leq_subr.
 set x2 := iter i face x1 => rt2 rs2 ru2 p2 b1ru2 Exp2.
 case: ifP => [lt_rt_nt _ | _ /andP[]].
@@ -356,9 +356,9 @@ Lemma iter_hub_subn i j :
      j < nhub -> forall x : G, arity x = nhub ->
   iter (hub_subn i j) face (iter j face x) = iter i face x.
 Proof.
-move=> ltjn x nFx; rewrite -iter_add subnK //; last first.
+move=> ltjn x nFx; rewrite -iterD subnK //; last first.
   by case: ifP => // _; rewrite ltnW ?ltn_addl.
-by case: ifP => _ //;  rewrite iter_add -nFx iter_face_arity.
+by case: ifP => _ //;  rewrite iterD -nFx iter_face_arity.
 Qed.
 
 Fixpoint hubcap_fit (p : part) (hc : hubcap) : bool :=

theories/initctree.v

@@ -158,7 +158,7 @@ have{Dtab ltab Dltab} [Dsz sub_ok]: h' + size tab = h.+1
   case: (nth _ _ i) => t0 t1; case: {i tab}(nth _ _ i) => t2 t3.
   do 2![move=> t_ok; move: {t_ok}(t_ok false) (t_ok true) => /= ? ?].
   by case: b0; rewrite /= -Dctp'; apply ctree_cons_proper.
-have{h Dh Dsz} Dsz: size tab = 2 by apply: (@addnI h'); rewrite Dsz Dh addn2.
+have{h Dh}{} Dsz: size tab = 2 by apply: (@addnI h'); rewrite Dsz Dh addn2.
 case: tab Dsz => [|[t0 t1] [|[t2 t3] tab']] //= _ in sub_ok *.
 have ok1 := sub_ok 1 _ isT.
 move: {sub_ok ok1}(sub_ok 0 true isT) (ok1 false) (ok1 true).
@@ -201,7 +201,7 @@ have{ltab Dtab Dltab} [Dsz Dsub]: h' + size tab = h.+1
   rewrite cbit0_addc cbit0_ccons cbit1_addc cbit1_ccons.
   case: e; rewrite /= ?addbT ?addbF -1?addSnnS;
     by case: b0; rewrite /= ctree_sub_cons /= ?andbF ?add0n.
-have{Dsz} Dsz: size tab = 2 by apply: (@addnI h'); rewrite Dsz Dh addnC.
+have{} Dsz: size tab = 2 by apply: (@addnI h'); rewrite Dsz Dh addnC.
 case: tab Dsz => [|[t0 t1] [|[t2 t3] tab']] //= _ in Dsub *.
 move Dtec: {-}(even_trace et) => tec; rewrite /= ctree_sub_cons {h}Dh.
 case: et => [|e et] //= in Dtec *; rewrite eqSS.

theories/jordan.v

@@ -262,7 +262,7 @@ have{Lp1} [q1 [fxCq1 Lq1 Uq1 _ z1Fq1]]: exists q1, let q := fx :: q1 in
   - rewrite -cons_uniq -cat_cons cat_uniq Uq1; case: hasP => //= -[t q2t q1t].
     by rewrite (rfP x t _) ?q1Fx // -rf_q2 -map_cons map_f in p'Fx.
   - rewrite map_cat 2!inE mem_cat rf_q2 orbA rfF [lhs in lhs || _]orb_idr //.
-    by case/mapP=> {t}t q1t ->; rewrite (rfP x t _) ?q1Fx // mem_behead.
+    by case/mapP=> {}t q1t ->; rewrite (rfP x t _) ?q1Fx // mem_behead.
   rewrite belast_cat -cat_cons mem_cat -q1Fx /= -cat_rcons -lastI -cface1r.
   by rewrite [t \in _]inE mem_cat orbCA -q1Fx; case: (cface x t) => // /z1Fq2.
 have{rf rfP rfF simple Sp1} p1'fx: fx \notin x :: p1.
@@ -288,8 +288,8 @@ have [p2 []]: exists p2, [/\ fpath edge y p2, last y p2 = nfx & z1 \notin p2].
   move: p1p_fx z1Ep p'z1 Lp; rewrite mem_cat (negPf p1'fx).
   case/splitPr: p / => p p2; rewrite cat_path /= => /and3P[_ _ fxEp2].
   by rewrite mem_cat last_cat => /norP[_ /norP[_]]; exists p2.
-elim: p2 y => [|_ p IHp y /andP[/eqP<- /IHp{IHp}IHp Lp]]; first by exists nil.
-rewrite inE => /norP[ey'z1 /(IHp Lp){p IHp Lp}IHp].
+elim: p2 y => [|_ p IHp y /andP[/eqP<- /IHp{}IHp Lp]]; first by exists nil.
+rewrite inE => /norP[ey'z1 /(IHp Lp){p Lp}{}IHp].
 apply: (@proj2 (y != nfx)); pose fey := face (edge y).
 have /connectP[q]: fconnect node y fey by rewrite cnode1r edgeK.
 elim: q (y) => /= [_ _ <- | _ q IHq z /andP[/eqP<- /IHq-IHz] /IHz{IHq IHz IHp}].

theories/kempe.v

@@ -199,7 +199,7 @@ set fz := face z in Dfz; set ez := edge z in Lp1; pose nez := node ez.
 pose ez' : WalkupN z := Sub ez (negbT (e'id _)).
 have eez': edge ez' = ez' by apply: val_inj; rewrite /= ee eqxx.
 pose H := WalkupE ez'; pose h (u : H) : G := sval (sval u).
-have{n IHn leGn} /IHn-IH_H: #|H| < n by rewrite ltnW // -!card_S_Walkup.
+have{n leGn} {}/IHn-IH_H: #|H| < n by rewrite ltnW // -!card_S_Walkup.
 have invh x: x != z -> x != ez -> {u | h u = x}.
   by move=> z'x ez'x; apply: exist (Sub (Sub x _ : WalkupN z) _) _.
 have h_eqE u v: (h u == h v) = (u == v) by [].

theories/kempetree.v

@@ -178,7 +178,7 @@ elim: d => [|d IHd] /= in ctu ctr gtu *.
     rewrite Pgtr andbC; case gt_w: (gtr_mem _ w) => [] => [_ | /negbFE//].
     by move: gt_w; rewrite -Dctrr /= orbF => /has_matchP[et /Dctr[]]; exists et.
   split=> [|et /= Pet].
-    case: ctu_lt_sz => [|[{Dctr}Dctr _]]; [by left | right; split=> // w].
+    case: ctu_lt_sz => [|[{}Dctr _]]; [by left | right; split=> // w].
     by rewrite Pgtr -Dctrr Dctr /= andbC; case: has_matchP => // [] [].
   right; apply/eqP/match_countP=> [[w gt_w wMet]]; case/negP: (Pgt w).
   rewrite gt_w; case gtu_w: (gtree_mem gtu w); last by rewrite orbT.
@@ -214,7 +214,7 @@ suffices{IHktc'} [gt_valid gt_full]:
     & forall sz, Kempe_complete sz.+1 ctu CtreeEmpty gtr gtu ->
       Kempe_complete sz ctu' (ctree_rotlr ctr) GtreeEmpty gtu].
 - by case/IHktc': gt_valid; split=> // sz; rewrite addnS => /gt_full; move: sz.
-have{Dctu'} Dctu': ctree_sub ctu' =1 even_fun et (sub_gt gtu et).
+have{} Dctu': ctree_sub ctu' =1 even_fun et (sub_gt gtu et).
   by move=> et; rewrite Dctu' Dctu addn0; case: ifP; rewrite ?addKn.
 split=> [|sz [ctu_lt_sz ctr_closed]].
   split=> // [|et0 ct_et0 | [] //].