From 990b2e9a81b97c261461c1da98f6890ee20c053c Mon Sep 17 00:00:00 2001
From: Yves Bertot <Yves.Bertot@inria.fr>
Date: Sun, 13 Mar 2022 21:14:49 +0100
Subject: [PATCH 1/5] removed deprecation warnings and most duplicate clear
 warnings

---
 theories/approx.v          |  2 +-
 theories/birkhoff.v        |  4 +-
 theories/cfcolor.v         |  2 +-
 theories/cfcontract.v      | 10 ++--
 theories/cfmap.v           |  4 +-
 theories/cfquiz.v          |  6 +--
 theories/cube.v            |  2 +-
 theories/dedekind.v        |  5 +-
 theories/discretize.v      |  4 +-
 theories/embed.v           |  2 +-
 theories/finitize.v        |  2 +-
 theories/geometry.v        |  2 +-
 theories/grid.v            |  5 +-
 theories/gridmap.v         |  2 +-
 theories/gtreerestrict.v   |  2 +-
 theories/hubcap.v          |  8 ++--
 theories/initctree.v       |  4 +-
 theories/jordan.v          |  6 +--
 theories/kempetree.v       |  4 +-
 theories/matte.v           |  2 +-
 theories/part.v            | 11 +++--
 theories/present.v         |  4 +-
 theories/quiz.v            |  2 +-
 theories/quiztree.v        |  2 +-
 theories/realcategorical.v |  2 +-
 theories/realprop.v        | 93 +++++++++++++++++++++++---------------
 theories/realsyntax.v      |  2 +
 theories/redpart.v         |  8 ++--
 theories/snip.v            |  2 +-
 theories/walkup.v          | 14 +++---
 30 files changed, 122 insertions(+), 96 deletions(-)

diff --git a/theories/approx.v b/theories/approx.v
index 4ad73fd..400a439 100644
--- a/theories/approx.v
+++ b/theories/approx.v
@@ -93,7 +93,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.
diff --git a/theories/birkhoff.v b/theories/birkhoff.v
index 2ef7223..c1336a8 100644
--- a/theories/birkhoff.v
+++ b/theories/birkhoff.v
@@ -309,7 +309,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.
@@ -331,7 +331,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.
diff --git a/theories/cfcolor.v b/theories/cfcolor.v
index 3253f7e..3beb288 100644
--- a/theories/cfcolor.v
+++ b/theories/cfcolor.v
@@ -378,7 +378,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.
diff --git a/theories/cfcontract.v b/theories/cfcontract.v
index 9369a8f..1935a92 100644
--- a/theories/cfcontract.v
+++ b/theories/cfcontract.v
@@ -103,7 +103,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.
@@ -731,7 +731,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)).
@@ -763,7 +763,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 [].
@@ -987,7 +987,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 /=.
@@ -1016,7 +1016,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.
diff --git a/theories/cfmap.v b/theories/cfmap.v
index f1b15c3..4343c56 100644
--- a/theories/cfmap.v
+++ b/theories/cfmap.v
@@ -410,7 +410,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.
@@ -1472,7 +1472,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.
diff --git a/theories/cfquiz.v b/theories/cfquiz.v
index 1e8b8d8..74e5943 100644
--- a/theories/cfquiz.v
+++ b/theories/cfquiz.v
@@ -387,7 +387,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.
@@ -470,7 +470,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 //.
@@ -639,7 +639,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 //=.
diff --git a/theories/cube.v b/theories/cube.v
index 014349a..e3b2437 100644
--- a/theories/cube.v
+++ b/theories/cube.v
@@ -175,7 +175,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 _].
diff --git a/theories/dedekind.v b/theories/dedekind.v
index 2184d27..488e7c9 100644
--- a/theories/dedekind.v
+++ b/theories/dedekind.v
@@ -51,6 +51,7 @@ Implicit Types n i : nat.
 
 (* Dedekind cuts. *)
 
+Declare Scope cut_scope.
 Delimit Scope cut_scope with cut.
 Open Scope cut_scope.
 
@@ -114,7 +115,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.
 
@@ -516,7 +517,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 //.
diff --git a/theories/discretize.v b/theories/discretize.v
index bf28b85..42e923e 100644
--- a/theories/discretize.v
+++ b/theories/discretize.v
@@ -199,7 +199,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.
@@ -369,7 +369,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.
diff --git a/theories/embed.v b/theories/embed.v
index c69b2e8..c020be8 100644
--- a/theories/embed.v
+++ b/theories/embed.v
@@ -1385,7 +1385,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)).
diff --git a/theories/finitize.v b/theories/finitize.v
index bfbeab6..027c0db 100644
--- a/theories/finitize.v
+++ b/theories/finitize.v
@@ -154,7 +154,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.
diff --git a/theories/geometry.v b/theories/geometry.v
index ce78fe0..114ad9a 100644
--- a/theories/geometry.v
+++ b/theories/geometry.v
@@ -155,7 +155,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.
diff --git a/theories/grid.v b/theories/grid.v
index 8cfc5bc..8770f3a 100644
--- a/theories/grid.v
+++ b/theories/grid.v
@@ -172,7 +172,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.
 
@@ -583,5 +583,6 @@ Qed.
 
 End GridGeometry.
 
-Hint Resolve oddgP.
+#[export]
+Hint Resolve oddgP : core.
 Arguments insetP {r p}.
diff --git a/theories/gridmap.v b/theories/gridmap.v
index c9d2ada..260d798 100644
--- a/theories/gridmap.v
+++ b/theories/gridmap.v
@@ -571,7 +571,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.
diff --git a/theories/gtreerestrict.v b/theories/gtreerestrict.v
index 58b6329..34e2b61 100644
--- a/theories/gtreerestrict.v
+++ b/theories/gtreerestrict.v
@@ -268,7 +268,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.
diff --git a/theories/hubcap.v b/theories/hubcap.v
index 6505500..8447834 100644
--- a/theories/hubcap.v
+++ b/theories/hubcap.v
@@ -211,7 +211,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.
@@ -275,7 +275,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[]].
@@ -353,9 +353,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 :=
diff --git a/theories/initctree.v b/theories/initctree.v
index 5f400b3..528008b 100644
--- a/theories/initctree.v
+++ b/theories/initctree.v
@@ -155,7 +155,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).
@@ -198,7 +198,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.
diff --git a/theories/jordan.v b/theories/jordan.v
index dc047a8..ad5a20c 100644
--- a/theories/jordan.v
+++ b/theories/jordan.v
@@ -260,7 +260,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.
@@ -286,8 +286,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}].
diff --git a/theories/kempetree.v b/theories/kempetree.v
index b99b5be..2123a6f 100644
--- a/theories/kempetree.v
+++ b/theories/kempetree.v
@@ -176,7 +176,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.
@@ -212,7 +212,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 | [] //].
diff --git a/theories/matte.v b/theories/matte.v
index d9498e7..93f4275 100644
--- a/theories/matte.v
+++ b/theories/matte.v
@@ -644,7 +644,7 @@ have [m_p6 | p6'm] := boolP (has (ehex (nd p)) m).
     right with (nd p) m => //; first by left.
     by rewrite in_mring inE gedge2 h_nd m_ep.
   by move=> q /predU1P[->|m_q]; [rewrite h_nd inE r_p | apply/orP; right].
-have [m_p | {m'p}m'p] := boolP (has (gtouch p) m); last first.
+have [m_p | {}m'p] := boolP (has (gtouch p) m); last first.
   suffices: has [pred q | has (predD r0 (gchop1 q)) m] (traject gface (nd p) 4).
     case/hasP/sig2W=> _ /trajectP/sig2_eqW[i _ ->].
     by apply: IHp; rewrite halfg_iter_face.
diff --git a/theories/part.v b/theories/part.v
index 8a1697f..5d77b19 100644
--- a/theories/part.v
+++ b/theories/part.v
@@ -172,6 +172,9 @@ Notation "8" := 8 (at level 0) : nat_scope.
 
 Module PartSyntax.
 
+Declare Scope prange_scope.
+Declare Scope part_scope.
+
 Notation "5" := Pr55 (at level 0) : prange_scope.
 Notation "6" := Pr66 (at level 0) : prange_scope.
 Notation "7" := Pr77 (at level 0) : prange_scope.
@@ -953,7 +956,7 @@ rewrite /rot_part -{1}(cat_take_drop_part n p) !fitp_cat andbC.
 congr (_ && _); congr (fitp _ _).
   congr (iter _ face x); move: (congr1 size_part (cat_take_drop_part n p)).
   by rewrite -(subnKC le_n_p) size_cat_part size_drop_part; apply: addIn.
-by rewrite -iter_add size_drop_part subnK // -nFx iter_face_arity.
+by rewrite -iterD size_drop_part subnK // -nFx iter_face_arity.
 Qed.
 
 Lemma fitp_catrev x p1 p2 :
@@ -1170,7 +1173,7 @@ have: let: (h45, q4) := conv_part4 p1 in
   rewrite fEnne -arity_face nodeK fEnne De2 -eEnf fEnne /effx De2 -eEnf.
   rewrite -{1}[edge (face x)](iter_face_subn (ltnW (ltnW (pentaG _)))).
   set n := arity (edge (face x)).
-  rewrite -iter_add addnC iter_add {1}[Pcons]lock /= !faceK -eEnf -lock.
+  rewrite -iterD addnC iterD {1}[Pcons]lock /= !faceK -eEnf -lock.
   have En: arity (edge (node (edge (face x)))) = n by rewrite -arity_face nodeK.
   rewrite -[edge x]nodeK arity_face -[node (edge x)]nodeK -fEnne in Eh34.
   case: p2 fit_p2 => [|s4 f41 p|f41 h45 p|f41 f42 h45 p|h' f1 f2 f3 p];
@@ -1189,7 +1192,7 @@ have{fit_p3 Eh45}: let: (u, q5) := conv_part5 h45 p3 in
     by rewrite -/effx Eh45 /= andbT => /and3P[Eu Es5 _].
   rewrite -/effx Eh45 !pentaG /= andbT => /andP[Eu].
   by rewrite !andbA andbC -!andbA => /andP[].
-case: {p3 h45}(conv_part5 h45 p3) => [u q5] [Eu {fit_q4}/fit_q4].
+case: {p3 h45}(conv_part5 h45 p3) => [u q5] [Eu {}/fit_q4].
 move: {q4 q5}(q4 q5) => q fit_q.
 move: (drop_part 3 p1) (fitp_drop 3 fit_p1) => p4; rewrite [_ x]/= => fit_p4.
 have{fit_p4}: let: (h23, q12) := conv_part12 p4 in
@@ -1223,7 +1226,7 @@ have{fit_p4}: let: (h23, q12) := conv_part12 p4 in
   by split; last by rewrite Dn Es1 Eh12 Ef21 Ef22 /inv_face2 !nodeK.
 case: {p4}(conv_part12 p4) => [h23 q12] [Eh23 fit_q12].
 move: (drop_part 5 p1) (size_drop_part 5 p1) (fitp_drop 5 fit_p1) => p6 Ep6.
-have{Ep6 Ep1} Ep6: arity x = 5 + size_part p6 by rewrite Ep6 -(eqP Ep1) subnKC.
+have{Ep1}{}Ep6: arity x = 5 + size_part p6 by rewrite Ep6 -(eqP Ep1) subnKC.
 move=> /= fit_p6.
 rewrite -2!arity_face {1}/inv_face2 !nodeK Eu /=; apply: {q12}fit_q12.
 case: p6 fit_p6 Ep6 => //= [_ Ex5 | f31 _ p7 /and3P[Ef31 _]].
diff --git a/theories/present.v b/theories/present.v
index 77ea1b3..985e46c 100644
--- a/theories/present.v
+++ b/theories/present.v
@@ -121,8 +121,8 @@ have fitp_split x (x_ok : valid_hub x) := fitp_split (proj1 x_ok) _ _ x.
 have p0lpl: forced_part p0l pl.
   rewrite /p0l; case: ifP => [p0ijk | _] G x x_ok //.
   by rewrite !fitp_split // => /andP[-> /p0p->].
-have{pl_ok} pl_ok: successful pl by apply: pl_ok.
-have{p0lpl pr_ok} pr_ok: successful pr.
+have {}pl_ok: successful pl by apply: pl_ok.
+have{p0lpl}{}pr_ok: successful pr.
   apply: pr_ok => G x x_ok => [|p0x]; have:= pl_ok G x x_ok.
     exact/contra/p0lpl.
   by rewrite !fitp_split // p0p ?andbT ?addNb.
diff --git a/theories/quiz.v b/theories/quiz.v
index eddc9ba..7c5fc59 100644
--- a/theories/quiz.v
+++ b/theories/quiz.v
@@ -473,7 +473,7 @@ have ccRa2: rlink_connected [predI fband a2 & hc].
   - move=> x y; rewrite !inE !fband_cons !orbF => /andP[xFx0 _] /andP[yFx0 _].
     by exists [::]; rewrite //= /rlink faceK (same_cface xFx0) cfaceC yFx0.
   by rewrite -{1}[x0c]e2c edgeK.
-have{Dac} Dac: ac =i fband a2.
+have {}Dac: ac =i fband a2.
   by move=> x; rewrite -Dac !(fband_cons, fband_cat); do !bool_congr.
 move=> x y; rewrite !(Dac, inE) => a2Fx a2Fy.
 have [p nfxRp a2_p] := ccRa2 _ _ a2Fx a2Fy.
diff --git a/theories/quiztree.v b/theories/quiztree.v
index 8518214..fb18763 100644
--- a/theories/quiztree.v
+++ b/theories/quiztree.v
@@ -293,7 +293,7 @@ Lemma qzt_fit_store_cf qz sym t :
  \/ qzt_fit t.
 Proof.
 rewrite /store_cf_qz /=; case: sym; do!case/qzt_fit_store; try tauto.
-case=> qzR [y]; have{qzR} qzR: isQuizR qz by case: (qz) qzR => q1 []; case: q1.
+case=> qzR [y]; have{} qzR: isQuizR qz by case: (qz) qzR => q1 []; case: q1.
 by rewrite fitqz_flip //; left; split; last by right; exists (face y).
 Qed.
 
diff --git a/theories/realcategorical.v b/theories/realcategorical.v
index 7a529f0..a4a6894 100644
--- a/theories/realcategorical.v
+++ b/theories/realcategorical.v
@@ -36,7 +36,7 @@ Import Order.TTheory GRing.Theory Num.Theory.
 
 Section RealsCategorical.
 
-Hint Resolve eqR_refl leRR.
+Hint Resolve eqR_refl leRR : core.
 
 Local Open Scope real_scope.
 
diff --git a/theories/realprop.v b/theories/realprop.v
index a71ffd2..4fa7366 100644
--- a/theories/realprop.v
+++ b/theories/realprop.v
@@ -29,7 +29,8 @@ Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
 Import Order.TTheory GRing.Theory Num.Theory.
-Hint Resolve iff_refl.
+#[export]
+Hint Resolve iff_refl : core.
 Local Open Scope real_scope.
 
 Local Notation "m %:Z" := m%:Z%R%N (only parsing).
@@ -86,7 +87,7 @@ Local Notation eqRset := (pointwise_relation Rtype iff).
 
 Lemma leRR x : x <= x.
 Proof. exact: (Real.le_reflexive R). Qed.
-Hint Resolve leRR.
+Hint Resolve leRR : core.
 
 Lemma leR_trans x y z : x <= y -> y <= z -> x <= z.
 Proof. exact: (Real.le_transitive R). Qed.
@@ -119,7 +120,7 @@ by case: (leR_total x y) => leyx neq_xy; [left | right] => lexy; case: neq_xy.
 Qed.
 
 Lemma ltRW x y : x < y -> x <= y. Proof. by have [] := leR_total x y. Qed.
-Hint Resolve ltRW.
+Hint Resolve ltRW : core.
 
 Lemma leR_lt_trans x y z : x <= y -> y < z -> x < z.
 Proof. by move=> lexy ltyz lezx; have:= leR_trans lezx lexy. Qed.
@@ -135,12 +136,12 @@ Proof. by move/ltRW; apply: leR_lt_trans. Qed.
 (**********************************************************)
 
 Lemma eqR_refl x : x == x. Proof. by []. Qed.
-Hint Resolve eqR_refl.
+Hint Resolve eqR_refl : core.
 
 Lemma eqR_congr x y : x = y -> x == y. Proof. by move->. Qed.
 
 Lemma eqR_sym x y : x == y -> y == x. Proof. by case. Qed.
-Hint Immediate eqR_sym.
+Hint Immediate eqR_sym : core.
 
 Lemma eqR_trans x y z : x == y -> y == z -> x == z.
 Proof. by move=> [lexy leyx] [/(leR_trans lexy)lexz /leR_trans/(_ leyx)]. Qed.
@@ -151,6 +152,7 @@ Add Parametric Relation : R eqR
   transitivity proved by eqR_trans
   as real_equality.
 
+#[export]
 Instance leR_Proper : Proper (eqR ==> eqR ==> iff) Real.le.
 Proof.
 move=> x1 x2 [lex12 lex21] y1 y2 [ley12 ley21].
@@ -164,6 +166,7 @@ Qed.
 Lemma addRC x y : x + y == y + x.
 Proof. exact: (Real.add_commutative R). Qed.
 
+#[export]
 Instance addR_Proper : Proper (eqR ==> eqR ==> eqR) Real.add.
 Proof.
 move=> x1 x2 Dx y1 y2 Dy; apply: (@eqR_trans _ (x1 + y2)).
@@ -240,6 +243,7 @@ Proof. by rewrite -subR_ge0 oppRK addRC subR_ge0. Qed.
 Lemma oppR_inj x y : - x == - y -> x == y.
 Proof. by rewrite /eqR !leR_opp2 => /eqR_sym. Qed.
 
+#[export]
 Instance oppR_Proper : Proper (eqR ==> eqR) Real.opp.
 Proof. by move=> x1 x2 Dx; apply: oppR_inj; rewrite !oppRK. Qed.
 
@@ -256,6 +260,7 @@ Proof. exact: (Real.mul_distributive_right R). Qed.
 Lemma mulRDl x y z : (y + z) * x == y * x + z * x.
 Proof. by rewrite -!(mulRC x) -mulRDr. Qed.
 
+#[export]
 Instance mulR_Proper : Proper (eqR ==> eqR ==> eqR) Real.mul.
 Proof.
 have posMr x y z : 0 <= x -> y == z -> x * y == x * z.
@@ -317,7 +322,7 @@ case/ltR_total: neqR10 => // lt10 le10; case: lt10.
 have{le10} le0N1: (0 : R) <= -1 by rewrite -oppR0 leR_opp2.
 by have:= Real.mul_monotone R le0N1 le0N1; rewrite mulR0 mulN1R oppRK.
 Qed.
-Hint Resolve ltR01.
+Hint Resolve ltR01 : core.
 
 Lemma ltRS x : x < x + 1.
 Proof. by rewrite -subR_le0 (addRC x) addRK. Qed.
@@ -329,7 +334,7 @@ Arguments ltPR x : clear implicits.
 
 Lemma ltR02 : (0 : R) < 2.
 Proof. exact: ltR_trans ltR01 (ltRS 1). Qed.
-Hint Resolve ltR02.
+Hint Resolve ltR02 : core.
 Let leR02 : 0 <= 2 := ltRW ltR02.
 
 (* Excluded middle and minimality of sup follow from the properties of 2! *)
@@ -395,6 +400,7 @@ Proof. by move=> notP; case: IFR_cases => z [][]. Qed.
 
 End SelectR.
 
+#[export]
 Instance IFR_Proper : Proper (iff ==> eqR ==> eqR ==> eqR) Real.select.
 Proof.
 move=> P1 P2 defP x1 x2 Dx y1 y2 Dy.
@@ -452,6 +458,7 @@ Qed.
 Lemma mulIR x y z : x != 0 -> y * x == z * x -> y == z.
 Proof. by rewrite -!(mulRC x); apply: mulRI. Qed.
 
+#[export]
 Instance invR_Proper : Proper (eqR ==> eqR) Real.extended_inv.
 Proof.
 move=> x1 x2 Dx; have [x2_0 | nzx2] := reals_classic (x2 == 0).
@@ -527,23 +534,29 @@ move=> hasE; have [|ubEx] := reals_classic (Real.down E x); first by left.
 by right; apply: sup_le_ub => // y Ey; apply/ltRW=> lexy; case: ubEx; exists y.
 Qed.
 
+#[export]
 Instance nonempty_Proper : Proper (eqRset ==> iff) Real.nonempty.
 Proof. by move=> E F defE; rewrite /Real.nonempty; setoid_rewrite defE. Qed.
 
+#[export]
 Instance ub_Proper : Proper (eqRset ==> eqR ==> iff) Real.ub.
 Proof. by move=> E F defE x1 x2 Dx; split=> ub_x y /defE/ub_x; rewrite Dx. Qed.
 
+#[export]
 Instance down_Proper : Proper (eqRset ==> eqR ==> iff) Real.down.
 Proof.
 by move=> E F defE x1 x2 Dx; split=> -[y /defE]; rewrite (Dx, =^~ Dx); exists y.
 Qed.
 
+#[export]
 Instance has_ub_Proper : Proper (eqRset ==> iff) Real.has_ub.
 Proof. by move=> E F dE; split=> -[y]; exists y; rewrite (dE, =^~ dE). Qed.
 
+#[export]
 Instance has_sup_Proper : Proper (eqRset ==> iff) Real.has_sup.
 Proof. by move=> E F dE; rewrite /Real.has_sup dE. Qed.
 
+#[export]
 Instance sup_Proper : Proper (eqRset ==> eqR) sup.
 Proof.
 move=> E F eqEF; have [supE | trivE] := reals_classic (Real.has_sup E).
@@ -585,7 +598,7 @@ Proof. by case: (min x y) / IFR_cases => _ [][lemx ->] //; apply/ltRW. Qed.
 
 Lemma leR_minr : min x y <= y.
 Proof. by case: (min x y) / IFR_cases => _ [][lemy ->]. Qed.
-Hint Resolve leR_minl leR_minr.
+Hint Resolve leR_minl leR_minr : core.
 
 Lemma ltR_min z : z < min x y <-> z < x /\ z < y.
 Proof.
@@ -605,7 +618,7 @@ Proof. by case: (max x y) / IFR_cases => _ [][ltxm ->]//; apply/ltRW. Qed.
 
 Lemma leR_maxr : y <= max x y.
 Proof. by case: (max x y) / IFR_cases => _ [][leym ->]. Qed.
-Hint Resolve leR_maxl leR_maxr.
+Hint Resolve leR_maxl leR_maxr : core.
 
 Lemma ltR_max z : max x y < z <-> x < z /\ y < z.
 Proof.
@@ -622,9 +635,11 @@ Qed.
 
 End MinMaxReal.
 
+#[export]
 Instance min_Proper : Proper (eqR ==> eqR ==> eqR) min.
 Proof. by move=> x1 x2 Dx y1 y2 Dy; rewrite /min Dx Dy. Qed.
 
+#[export]
 Instance max_Proper : Proper (eqR ==> eqR ==> eqR) max.
 Proof. by move=> x1 x2 Dx y1 y2 Dy; rewrite /max Dx Dy. Qed.
 
@@ -641,7 +656,7 @@ Arguments ltR0Sn n : clear implicits.
 
 Lemma leR0n n : 0 <= n.
 Proof. by case: n => // n; apply/ltRW/ltR0Sn. Qed.
-Hint Resolve ltR0Sn leR0n.
+Hint Resolve ltR0Sn leR0n : core.
 
 Lemma intRN m : (- m)%R == - m.
 Proof. by case: m => [[|n]|n]; rewrite ?oppR0 ?oppRK. Qed.
@@ -758,11 +773,11 @@ Qed.
 
 Fact ub_floor_set x : Real.ub (floor_set x) x.
 Proof. by move=> y [m]. Qed.
-Hint Resolve ub_floor_set.
+Hint Resolve ub_floor_set : core.
 
 Fact has_ub_floor_set x : Real.has_ub (floor_set x).
 Proof. by exists x. Qed.
-Hint Resolve has_ub_floor_set.
+Hint Resolve has_ub_floor_set : core.
 
 Let has_floor_max x : Real.nonempty (floor_set x) -> x < floor x + 1.
 Proof.
@@ -786,17 +801,19 @@ rewrite -{2}(oppRK x) intRN leR_opp2 -{2}(subRK (- x) 1) !intRD1 leR_add2r.
 apply/leR_trans/ltRW; rewrite -(leR_add2r 1) subRK.
 by apply: has_floor_max; case: ub_nx0.
 Qed.
-Hint Resolve nonempty_floor_set.
+Hint Resolve nonempty_floor_set : core.
 
 Lemma has_sup_floor_set x : Real.has_sup (floor_set x). Proof. by []. Qed.
-Hint Resolve has_sup_floor_set.
+Hint Resolve has_sup_floor_set : core.
 
+#[export]
 Instance floor_Proper : Proper (eqR ==> eqR) floor.
 Proof.
 move=> x1 x2 Dx; apply: sup_Proper => y.
 by split=> -[m int_m_x]; split; rewrite (Dx, =^~ Dx).
 Qed.
 
+#[export]
 Instance range1_Proper : Proper (eqR ==> eqR ==> iff) range1.
 Proof. by move=> x1 x2 Dx y1 y2 Dy; rewrite /range1 Dx Dy. Qed.
 
@@ -861,6 +878,7 @@ move: lemx; rewrite -(leR_add2r (d1 * z)); apply: ltR_le_trans.
 by rewrite leR_add2l mulRC leR_pmul2l // /d1 intRS.
 Qed.
 
+#[export]
 Instance imageR_Proper (S : Real.structure) :
   Proper
     (pointwise_relation S eqR ==> pointwise_relation S iff ==> eqR ==> iff)
@@ -883,27 +901,28 @@ Arguments intR_ltP {R m1 m2}.
 Arguments ratR_leP {R a1 a2}.
 Arguments ratR_ltP {R a1 a2}.
 
-Hint Resolve eqR_refl leRR ltRW.
-
-Existing Instance real_equality.
-Existing Instance real_equality_Transitive.
-Existing Instance real_equality_Symmetric.
-Existing Instance real_equality_Reflexive.
-Existing Instance real_equality_relation.
-Existing Instance leR_Proper.
-Existing Instance addR_Proper.
-Existing Instance oppR_Proper.
-Existing Instance mulR_Proper.
-Existing Instance invR_Proper.
-Existing Instance IFR_Proper.
-Existing Instance nonempty_Proper.
-Existing Instance ub_Proper.
-Existing Instance has_ub_Proper.
-Existing Instance has_sup_Proper.
-Existing Instance sup_Proper.
-Existing Instance min_Proper.
-Existing Instance max_Proper.
-Existing Instance range1_Proper.
-Existing Instance floor_Proper.
-Existing Instance imageR_Proper.
+#[export]
+Hint Resolve eqR_refl leRR ltRW : core.
+
+#[export] Existing Instance real_equality.
+#[export] Existing Instance real_equality_Transitive.
+#[export] Existing Instance real_equality_Symmetric.
+#[export] Existing Instance real_equality_Reflexive.
+#[export] Existing Instance real_equality_relation.
+#[export] Existing Instance leR_Proper.
+#[export] Existing Instance addR_Proper.
+#[export] Existing Instance oppR_Proper.
+#[export] Existing Instance mulR_Proper.
+#[export] Existing Instance invR_Proper.
+#[export] Existing Instance IFR_Proper.
+#[export] Existing Instance nonempty_Proper.
+#[export] Existing Instance ub_Proper.
+#[export] Existing Instance has_ub_Proper.
+#[export] Existing Instance has_sup_Proper.
+#[export] Existing Instance sup_Proper.
+#[export] Existing Instance min_Proper.
+#[export] Existing Instance max_Proper.
+#[export] Existing Instance range1_Proper.
+#[export] Existing Instance floor_Proper.
+#[export] Existing Instance imageR_Proper.
 
diff --git a/theories/realsyntax.v b/theories/realsyntax.v
index 2acdb75..218fbdd 100644
--- a/theories/realsyntax.v
+++ b/theories/realsyntax.v
@@ -35,6 +35,8 @@ From fourcolor Require Import real.
 Import Real.
 Export RealCoercions.
 
+Declare Scope real_scope.
+Declare Scope realset_scope.
 Bind Scope real_scope with val.
 Bind Scope realset_scope with set.
 Delimit Scope real_scope with Rval.
diff --git a/theories/redpart.v b/theories/redpart.v
index 0f37fa7..16750e3 100644
--- a/theories/redpart.v
+++ b/theories/redpart.v
@@ -402,10 +402,10 @@ case: zp => zi' pl pr /(congr1 size_part).
 rewrite catrev_part_eq size_cat_part size_rev_part -iterS.
 case sz_pr: (size_part pr) => [|[|n]] sz_pl; rewrite ?addn0 ?addn1 in sz_pl.
 - rewrite {}sz_pl -zvalid_initr catrev_part_eq size_cat_part size_rev_part.
-  rewrite size_drop_part subn1 Ep0r -nFx0 -addnS iter_add [RHS]/=(f_finv faceI).
+  rewrite size_drop_part subn1 Ep0r -nFx0 -addnS iterD [RHS]/=(f_finv faceI).
   by case: pr sz_pr.
 - rewrite {}sz_pl -zvalid_init catrev_part_eq size_cat_part size_rev_part.
-  rewrite iter_add Ep0r -nFx0 iter_face_arity.
+  rewrite iterD Ep0r -nFx0 iter_face_arity.
   by case: pr sz_pr => // [s h|h f1|h f1 f2|h f1 f2 f3] [].
 by case: pr sz_pr => // [s h|h f1|h f1 f2|h f1 f2 f3] [].
 Qed.
@@ -664,10 +664,10 @@ apply/andP; split.
   move/eqP: (congr1 size_part Ep0r1); rewrite size_cat_part Ey eq_sym.
   by rewrite size_drop_part size_cat_part Ep0r addnK addnC eqn_add2r.
 suffices: fitp y p0r1 by rewrite -{1}Ep0r1 fitp_cat => /andP[].
-rewrite fitp_cat fit_pc // -iter_add addnC.
+rewrite fitp_cat fit_pc // -iterD addnC.
 have [-> _] := Dpcj (popqa r) pr; rewrite -{}Epr -(size_rev_part pl).
 rewrite -size_cat_part -catrev_part_eq p_ok size_cat_part  Ep0r -nFx0.
-by rewrite iter_add !iter_face_arity.
+by rewrite iterD !iter_face_arity.
 Qed.
 
 Definition red_popr_spoke pr :=
diff --git a/theories/snip.v b/theories/snip.v
index f60c3da..7a51c87 100644
--- a/theories/snip.v
+++ b/theories/snip.v
@@ -234,7 +234,7 @@ have [x1 c_nx1 [p [x1Cp Lp] Upc]]: exists2 x1, node x1 \in z' :: c
     by apply: sub_path x1Dp => t u /andP[].
   rewrite has_rcons orbCA negb_or Ucp andbT.
   by apply: contra Uq1c; rewrite has_sym /= => ->.
-have{z'Cc} z'Cc: path clink z' c.
+have{} z'Cc: path clink z' c.
   apply: sub_path z'Cc => t _ /eqP <- /=.
   by case: ifP => _; [rewrite -{1}[t]edgeK clinkN | rewrite clinkF].
 have [c0 [x1Cc0 Lc0] Ucc0]: exists2 c0,
diff --git a/theories/walkup.v b/theories/walkup.v
index 02c6edd..381f636 100644
--- a/theories/walkup.v
+++ b/theories/walkup.v
@@ -538,14 +538,14 @@ have{uCq} xCp: path clink2 x p; last move {u q} in (p) (x) (y) Uzp xCp pynx Lp.
 have [p'x Up]: x \notin p /\ uniq p by case/and3P: Uzp.
 have y'x: x != y by rewrite (memPnC p'x) // (mem2l pynx).
 have not_xCp: ~~ path clink x p.
-  apply: contra (JordanG (x :: p)) => {xCp}xCp; rewrite /= p'x Up xCp /=.
+  apply: contra (JordanG (x :: p)) => {} xCp; rewrite /= p'x Up xCp /=.
   case: eqP => [y_t | _] in Lp; rewrite Lp GnK; last first.
     case: eqP => // x_t in pynx; have/and3P[] := JordanG [:: z, x & p].
     by rewrite Uzp /= Lp GnK -cat1s mem2_cat pynx orbT xCp x_t zCt.
   have/and3P[] := JordanG (x :: rcons p z); rewrite last_rcons -/t -y_t.
   rewrite rcons_path xCp Lp clinkN -cats1 -cat_cons uniq_catC Uzp.
   by rewrite -y_t ifN // in pynx; rewrite mem2_cat pynx.
-have{not_xCp y'x} not_xCp: ~~ path clink1 x p.
+have{y'x} {}not_xCp: ~~ path clink1 x p.
   apply/negP=> /cpath1P[] {not_xCp}// p1 [p2 [_ Dp Lp2 xCp1 zCp2]]. 
   rewrite Dp -cat_cons uniq_catCA in Uzp.
   have /and3P[] := JordanG (x :: p1 ++ z :: p2); rewrite Uzp last_cat /= Lp2.
@@ -560,23 +560,23 @@ have{not_xCp y'x} not_xCp: ~~ path clink1 x p.
   rewrite xCp1 last_rcons -cats1 (subseq_uniq _ Uzp) ?catA ?prefix_subseq //.
   by rewrite -y_t ifN // Dp mem2r_cat // y_t in pynx; rewrite mem2_cat pynx.
 have p_t: t \in p by apply: contraR (cpath1I x p _) _.
-have{pynx p'x} pynx: mem2 p y (node x) by rewrite ifN ?(memPnC p'x) in pynx.
+have{p'x} {}pynx: mem2 p y (node x) by rewrite ifN ?(memPnC p'x) in pynx.
 do [have{p p_t} [p1 p2] := splitPr p_t] in Uzp Up Lp xCp not_xCp pynx.
 rewrite !cat_path cat_uniq /= has_sym -cons_uniq in Up xCp not_xCp.
 have [[xCp1 p1Ct tCp2] [Up1 /norP[p1't Up21] Utp2]] := (and3P xCp, and3P Up).
 have{xCp Up} [p2't Up2]: t \notin p2 /\ uniq p2 by case/andP: Utp2.
-have{xCp1 p1't} xCp1: path clink1 x p1 by rewrite cpath1I.
-have{tCp2 p2't cpath1I} tCp2: path clink1 t p2 by rewrite cpath1I.
+have{p1't} {}xCp1: path clink1 x p1 by rewrite cpath1I.
+have{p2't cpath1I} {}tCp2: path clink1 t p2 by rewrite cpath1I.
 have{not_xCp p1Ct} Lp1: last x p1 = node z.
   case/predU1P: p1Ct => [-> /= | p1Ft]; first by rewrite nt_z eqxx.
   by rewrite xCp1 tCp2 /clink1 p1Ft orbT in not_xCp.
 have{Lp} [Lp2 t'y]: last t p2 = node y /\ y != t.
   case: ifPn Lp Uzp; rewrite (lastI x) last_cat => //= _ -> /nandP[]; right.
   by rewrite belast_cat Lp1 rcons_uniq mem_cat mem_head orbT.
-have{xCp1 Up21} xCp1: path clink x p1.
+have{Up21} {}xCp1: path clink x p1.
   apply/idPn=> /cpath1P[] {xCp1}// q1 [q2 [p1fz Dp1 Lq2 xCq1 zCq2]].
   rewrite {}Dp1 cat_uniq -catA -cat_cons uniq_catCA catA cats1 in Up1 Uzp pynx.
-  have{tCp2 p1fz} tCp2: path clink t p2 by rewrite cpathI ?(hasPn Up21).
+  have{p1fz} {}tCp2: path clink t p2 by rewrite cpathI ?(hasPn Up21).
   have q2'nx: node x \notin q2.
     apply: contra (JordanG (x :: rcons q1 z ++ q2)) => q2nx; apply/and3P.
     rewrite (subseq_uniq _ Uzp) ?catA ?prefix_subseq // last_cat cat_path xCq1.

From 05250dda607b35a4e834935e5a3d95002bfa3482 Mon Sep 17 00:00:00 2001
From: Yves Bertot <Yves.Bertot@inria.fr>
Date: Fri, 25 Mar 2022 16:00:00 +0100
Subject: [PATCH 2/5] removes some deprecation warnings and duplicate-clear
 warnings, but retains compatibility with coq-8.11 and math-comp 1.11

---
 theories/cfcolor.v    |  2 +-
 theories/cfcontract.v |  2 +-
 theories/cfmap.v      |  2 +-
 theories/cfquiz.v     |  4 +--
 theories/cube.v       |  2 +-
 theories/geometry.v   |  2 +-
 theories/grid.v       |  1 -
 theories/hubcap.v     |  6 ++---
 theories/initctree.v  |  2 +-
 theories/kempetree.v  |  2 +-
 theories/part.v       |  4 +--
 theories/quiztree.v   |  2 +-
 theories/realprop.v   | 61 +++++++++++++++----------------------------
 theories/redpart.v    |  8 +++---
 theories/snip.v       |  2 +-
 15 files changed, 41 insertions(+), 61 deletions(-)

diff --git a/theories/cfcolor.v b/theories/cfcolor.v
index 3beb288..c157c42 100644
--- a/theories/cfcolor.v
+++ b/theories/cfcolor.v
@@ -378,7 +378,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 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.
diff --git a/theories/cfcontract.v b/theories/cfcontract.v
index 1935a92..e2a41d0 100644
--- a/theories/cfcontract.v
+++ b/theories/cfcontract.v
@@ -1016,7 +1016,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 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.
diff --git a/theories/cfmap.v b/theories/cfmap.v
index 4343c56..baad756 100644
--- a/theories/cfmap.v
+++ b/theories/cfmap.v
@@ -1472,7 +1472,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: 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.
diff --git a/theories/cfquiz.v b/theories/cfquiz.v
index 74e5943..771db9a 100644
--- a/theories/cfquiz.v
+++ b/theories/cfquiz.v
@@ -470,7 +470,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: 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 //.
@@ -639,7 +639,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: 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 //=.
diff --git a/theories/cube.v b/theories/cube.v
index e3b2437..1892354 100644
--- a/theories/cube.v
+++ b/theories/cube.v
@@ -175,7 +175,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 _ 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 _].
diff --git a/theories/geometry.v b/theories/geometry.v
index 114ad9a..ce78fe0 100644
--- a/theories/geometry.v
+++ b/theories/geometry.v
@@ -155,7 +155,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 -iterD subnK ?iter_face_arity. Qed.
+Proof. by move=> le_n_x; rewrite -iter_add 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.
diff --git a/theories/grid.v b/theories/grid.v
index 8770f3a..3fef0cd 100644
--- a/theories/grid.v
+++ b/theories/grid.v
@@ -583,6 +583,5 @@ Qed.
 
 End GridGeometry.
 
-#[export]
 Hint Resolve oddgP : core.
 Arguments insetP {r p}.
diff --git a/theories/hubcap.v b/theories/hubcap.v
index 8447834..580fd67 100644
--- a/theories/hubcap.v
+++ b/theories/hubcap.v
@@ -275,7 +275,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 -iterD subnK // -nFx1 iter_face_arity.
+    by rewrite -iter_add 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[]].
@@ -353,9 +353,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 -iterD subnK //; last first.
+move=> ltjn x nFx; rewrite -iter_add subnK //; last first.
   by case: ifP => // _; rewrite ltnW ?ltn_addl.
-by case: ifP => _ //;  rewrite iterD -nFx iter_face_arity.
+by case: ifP => _ //;  rewrite iter_add -nFx iter_face_arity.
 Qed.
 
 Fixpoint hubcap_fit (p : part) (hc : hubcap) : bool :=
diff --git a/theories/initctree.v b/theories/initctree.v
index 528008b..62410de 100644
--- a/theories/initctree.v
+++ b/theories/initctree.v
@@ -198,7 +198,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: 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.
diff --git a/theories/kempetree.v b/theories/kempetree.v
index 2123a6f..5e3708e 100644
--- a/theories/kempetree.v
+++ b/theories/kempetree.v
@@ -212,7 +212,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': 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 | [] //].
diff --git a/theories/part.v b/theories/part.v
index 5d77b19..b29fe36 100644
--- a/theories/part.v
+++ b/theories/part.v
@@ -956,7 +956,7 @@ rewrite /rot_part -{1}(cat_take_drop_part n p) !fitp_cat andbC.
 congr (_ && _); congr (fitp _ _).
   congr (iter _ face x); move: (congr1 size_part (cat_take_drop_part n p)).
   by rewrite -(subnKC le_n_p) size_cat_part size_drop_part; apply: addIn.
-by rewrite -iterD size_drop_part subnK // -nFx iter_face_arity.
+by rewrite -iter_add size_drop_part subnK // -nFx iter_face_arity.
 Qed.
 
 Lemma fitp_catrev x p1 p2 :
@@ -1173,7 +1173,7 @@ have: let: (h45, q4) := conv_part4 p1 in
   rewrite fEnne -arity_face nodeK fEnne De2 -eEnf fEnne /effx De2 -eEnf.
   rewrite -{1}[edge (face x)](iter_face_subn (ltnW (ltnW (pentaG _)))).
   set n := arity (edge (face x)).
-  rewrite -iterD addnC iterD {1}[Pcons]lock /= !faceK -eEnf -lock.
+  rewrite -iter_add addnC iter_add {1}[Pcons]lock /= !faceK -eEnf -lock.
   have En: arity (edge (node (edge (face x)))) = n by rewrite -arity_face nodeK.
   rewrite -[edge x]nodeK arity_face -[node (edge x)]nodeK -fEnne in Eh34.
   case: p2 fit_p2 => [|s4 f41 p|f41 h45 p|f41 f42 h45 p|h' f1 f2 f3 p];
diff --git a/theories/quiztree.v b/theories/quiztree.v
index fb18763..68eee9b 100644
--- a/theories/quiztree.v
+++ b/theories/quiztree.v
@@ -293,7 +293,7 @@ Lemma qzt_fit_store_cf qz sym t :
  \/ qzt_fit t.
 Proof.
 rewrite /store_cf_qz /=; case: sym; do!case/qzt_fit_store; try tauto.
-case=> qzR [y]; have{} qzR: isQuizR qz by case: (qz) qzR => q1 []; case: q1.
+case=> qzR [y]; have {}qzR: isQuizR qz by case: (qz) qzR => q1 []; case: q1.
 by rewrite fitqz_flip //; left; split; last by right; exists (face y).
 Qed.
 
diff --git a/theories/realprop.v b/theories/realprop.v
index 4fa7366..5408cb7 100644
--- a/theories/realprop.v
+++ b/theories/realprop.v
@@ -29,7 +29,6 @@ Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
 Import Order.TTheory GRing.Theory Num.Theory.
-#[export]
 Hint Resolve iff_refl : core.
 Local Open Scope real_scope.
 
@@ -152,7 +151,6 @@ Add Parametric Relation : R eqR
   transitivity proved by eqR_trans
   as real_equality.
 
-#[export]
 Instance leR_Proper : Proper (eqR ==> eqR ==> iff) Real.le.
 Proof.
 move=> x1 x2 [lex12 lex21] y1 y2 [ley12 ley21].
@@ -166,7 +164,6 @@ Qed.
 Lemma addRC x y : x + y == y + x.
 Proof. exact: (Real.add_commutative R). Qed.
 
-#[export]
 Instance addR_Proper : Proper (eqR ==> eqR ==> eqR) Real.add.
 Proof.
 move=> x1 x2 Dx y1 y2 Dy; apply: (@eqR_trans _ (x1 + y2)).
@@ -243,7 +240,6 @@ Proof. by rewrite -subR_ge0 oppRK addRC subR_ge0. Qed.
 Lemma oppR_inj x y : - x == - y -> x == y.
 Proof. by rewrite /eqR !leR_opp2 => /eqR_sym. Qed.
 
-#[export]
 Instance oppR_Proper : Proper (eqR ==> eqR) Real.opp.
 Proof. by move=> x1 x2 Dx; apply: oppR_inj; rewrite !oppRK. Qed.
 
@@ -260,7 +256,6 @@ Proof. exact: (Real.mul_distributive_right R). Qed.
 Lemma mulRDl x y z : (y + z) * x == y * x + z * x.
 Proof. by rewrite -!(mulRC x) -mulRDr. Qed.
 
-#[export]
 Instance mulR_Proper : Proper (eqR ==> eqR ==> eqR) Real.mul.
 Proof.
 have posMr x y z : 0 <= x -> y == z -> x * y == x * z.
@@ -400,7 +395,6 @@ Proof. by move=> notP; case: IFR_cases => z [][]. Qed.
 
 End SelectR.
 
-#[export]
 Instance IFR_Proper : Proper (iff ==> eqR ==> eqR ==> eqR) Real.select.
 Proof.
 move=> P1 P2 defP x1 x2 Dx y1 y2 Dy.
@@ -458,7 +452,6 @@ Qed.
 Lemma mulIR x y z : x != 0 -> y * x == z * x -> y == z.
 Proof. by rewrite -!(mulRC x); apply: mulRI. Qed.
 
-#[export]
 Instance invR_Proper : Proper (eqR ==> eqR) Real.extended_inv.
 Proof.
 move=> x1 x2 Dx; have [x2_0 | nzx2] := reals_classic (x2 == 0).
@@ -534,29 +527,23 @@ move=> hasE; have [|ubEx] := reals_classic (Real.down E x); first by left.
 by right; apply: sup_le_ub => // y Ey; apply/ltRW=> lexy; case: ubEx; exists y.
 Qed.
 
-#[export]
 Instance nonempty_Proper : Proper (eqRset ==> iff) Real.nonempty.
 Proof. by move=> E F defE; rewrite /Real.nonempty; setoid_rewrite defE. Qed.
 
-#[export]
 Instance ub_Proper : Proper (eqRset ==> eqR ==> iff) Real.ub.
 Proof. by move=> E F defE x1 x2 Dx; split=> ub_x y /defE/ub_x; rewrite Dx. Qed.
 
-#[export]
 Instance down_Proper : Proper (eqRset ==> eqR ==> iff) Real.down.
 Proof.
 by move=> E F defE x1 x2 Dx; split=> -[y /defE]; rewrite (Dx, =^~ Dx); exists y.
 Qed.
 
-#[export]
 Instance has_ub_Proper : Proper (eqRset ==> iff) Real.has_ub.
 Proof. by move=> E F dE; split=> -[y]; exists y; rewrite (dE, =^~ dE). Qed.
 
-#[export]
 Instance has_sup_Proper : Proper (eqRset ==> iff) Real.has_sup.
 Proof. by move=> E F dE; rewrite /Real.has_sup dE. Qed.
 
-#[export]
 Instance sup_Proper : Proper (eqRset ==> eqR) sup.
 Proof.
 move=> E F eqEF; have [supE | trivE] := reals_classic (Real.has_sup E).
@@ -635,11 +622,9 @@ Qed.
 
 End MinMaxReal.
 
-#[export]
 Instance min_Proper : Proper (eqR ==> eqR ==> eqR) min.
 Proof. by move=> x1 x2 Dx y1 y2 Dy; rewrite /min Dx Dy. Qed.
 
-#[export]
 Instance max_Proper : Proper (eqR ==> eqR ==> eqR) max.
 Proof. by move=> x1 x2 Dx y1 y2 Dy; rewrite /max Dx Dy. Qed.
 
@@ -806,14 +791,12 @@ Hint Resolve nonempty_floor_set : core.
 Lemma has_sup_floor_set x : Real.has_sup (floor_set x). Proof. by []. Qed.
 Hint Resolve has_sup_floor_set : core.
 
-#[export]
 Instance floor_Proper : Proper (eqR ==> eqR) floor.
 Proof.
 move=> x1 x2 Dx; apply: sup_Proper => y.
 by split=> -[m int_m_x]; split; rewrite (Dx, =^~ Dx).
 Qed.
 
-#[export]
 Instance range1_Proper : Proper (eqR ==> eqR ==> iff) range1.
 Proof. by move=> x1 x2 Dx y1 y2 Dy; rewrite /range1 Dx Dy. Qed.
 
@@ -878,7 +861,6 @@ move: lemx; rewrite -(leR_add2r (d1 * z)); apply: ltR_le_trans.
 by rewrite leR_add2l mulRC leR_pmul2l // /d1 intRS.
 Qed.
 
-#[export]
 Instance imageR_Proper (S : Real.structure) :
   Proper
     (pointwise_relation S eqR ==> pointwise_relation S iff ==> eqR ==> iff)
@@ -901,28 +883,27 @@ Arguments intR_ltP {R m1 m2}.
 Arguments ratR_leP {R a1 a2}.
 Arguments ratR_ltP {R a1 a2}.
 
-#[export]
 Hint Resolve eqR_refl leRR ltRW : core.
 
-#[export] Existing Instance real_equality.
-#[export] Existing Instance real_equality_Transitive.
-#[export] Existing Instance real_equality_Symmetric.
-#[export] Existing Instance real_equality_Reflexive.
-#[export] Existing Instance real_equality_relation.
-#[export] Existing Instance leR_Proper.
-#[export] Existing Instance addR_Proper.
-#[export] Existing Instance oppR_Proper.
-#[export] Existing Instance mulR_Proper.
-#[export] Existing Instance invR_Proper.
-#[export] Existing Instance IFR_Proper.
-#[export] Existing Instance nonempty_Proper.
-#[export] Existing Instance ub_Proper.
-#[export] Existing Instance has_ub_Proper.
-#[export] Existing Instance has_sup_Proper.
-#[export] Existing Instance sup_Proper.
-#[export] Existing Instance min_Proper.
-#[export] Existing Instance max_Proper.
-#[export] Existing Instance range1_Proper.
-#[export] Existing Instance floor_Proper.
-#[export] Existing Instance imageR_Proper.
+Existing Instance real_equality.
+Existing Instance real_equality_Transitive.
+Existing Instance real_equality_Symmetric.
+Existing Instance real_equality_Reflexive.
+Existing Instance real_equality_relation.
+Existing Instance leR_Proper.
+Existing Instance addR_Proper.
+Existing Instance oppR_Proper.
+Existing Instance mulR_Proper.
+Existing Instance invR_Proper.
+Existing Instance IFR_Proper.
+Existing Instance nonempty_Proper.
+Existing Instance ub_Proper.
+Existing Instance has_ub_Proper.
+Existing Instance has_sup_Proper.
+Existing Instance sup_Proper.
+Existing Instance min_Proper.
+Existing Instance max_Proper.
+Existing Instance range1_Proper.
+Existing Instance floor_Proper.
+Existing Instance imageR_Proper.
 
diff --git a/theories/redpart.v b/theories/redpart.v
index 16750e3..0f37fa7 100644
--- a/theories/redpart.v
+++ b/theories/redpart.v
@@ -402,10 +402,10 @@ case: zp => zi' pl pr /(congr1 size_part).
 rewrite catrev_part_eq size_cat_part size_rev_part -iterS.
 case sz_pr: (size_part pr) => [|[|n]] sz_pl; rewrite ?addn0 ?addn1 in sz_pl.
 - rewrite {}sz_pl -zvalid_initr catrev_part_eq size_cat_part size_rev_part.
-  rewrite size_drop_part subn1 Ep0r -nFx0 -addnS iterD [RHS]/=(f_finv faceI).
+  rewrite size_drop_part subn1 Ep0r -nFx0 -addnS iter_add [RHS]/=(f_finv faceI).
   by case: pr sz_pr.
 - rewrite {}sz_pl -zvalid_init catrev_part_eq size_cat_part size_rev_part.
-  rewrite iterD Ep0r -nFx0 iter_face_arity.
+  rewrite iter_add Ep0r -nFx0 iter_face_arity.
   by case: pr sz_pr => // [s h|h f1|h f1 f2|h f1 f2 f3] [].
 by case: pr sz_pr => // [s h|h f1|h f1 f2|h f1 f2 f3] [].
 Qed.
@@ -664,10 +664,10 @@ apply/andP; split.
   move/eqP: (congr1 size_part Ep0r1); rewrite size_cat_part Ey eq_sym.
   by rewrite size_drop_part size_cat_part Ep0r addnK addnC eqn_add2r.
 suffices: fitp y p0r1 by rewrite -{1}Ep0r1 fitp_cat => /andP[].
-rewrite fitp_cat fit_pc // -iterD addnC.
+rewrite fitp_cat fit_pc // -iter_add addnC.
 have [-> _] := Dpcj (popqa r) pr; rewrite -{}Epr -(size_rev_part pl).
 rewrite -size_cat_part -catrev_part_eq p_ok size_cat_part  Ep0r -nFx0.
-by rewrite iterD !iter_face_arity.
+by rewrite iter_add !iter_face_arity.
 Qed.
 
 Definition red_popr_spoke pr :=
diff --git a/theories/snip.v b/theories/snip.v
index 7a51c87..cf0b2ee 100644
--- a/theories/snip.v
+++ b/theories/snip.v
@@ -234,7 +234,7 @@ have [x1 c_nx1 [p [x1Cp Lp] Upc]]: exists2 x1, node x1 \in z' :: c
     by apply: sub_path x1Dp => t u /andP[].
   rewrite has_rcons orbCA negb_or Ucp andbT.
   by apply: contra Uq1c; rewrite has_sym /= => ->.
-have{} z'Cc: path clink z' c.
+have {}z'Cc: path clink z' c.
   apply: sub_path z'Cc => t _ /eqP <- /=.
   by case: ifP => _; [rewrite -{1}[t]edgeK clinkN | rewrite clinkF].
 have [c0 [x1Cc0 Lc0] Ucc0]: exists2 c0,

From 65ea0f2005c88aa2acddce0088a4ff6fabe737b1 Mon Sep 17 00:00:00 2001
From: Yves Bertot <Yves.Bertot@inria.fr>
Date: Mon, 28 Mar 2022 13:46:30 +0200
Subject: [PATCH 3/5] remove unidiomatic empty clears between curly brackets

---
 theories/birkhoff.v  | 4 ++--
 theories/initctree.v | 2 +-
 theories/jordan.v    | 2 +-
 theories/part.v      | 2 +-
 theories/present.v   | 2 +-
 5 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/theories/birkhoff.v b/theories/birkhoff.v
index c1336a8..7d4cbf5 100644
--- a/theories/birkhoff.v
+++ b/theories/birkhoff.v
@@ -309,7 +309,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 _.
+  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.
@@ -331,7 +331,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] {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.
diff --git a/theories/initctree.v b/theories/initctree.v
index 62410de..6e8f690 100644
--- a/theories/initctree.v
+++ b/theories/initctree.v
@@ -155,7 +155,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: 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).
diff --git a/theories/jordan.v b/theories/jordan.v
index ad5a20c..c816d8e 100644
--- a/theories/jordan.v
+++ b/theories/jordan.v
@@ -287,7 +287,7 @@ have [p2 []]: exists p2, [/\ fpath edge y p2, last y p2 = nfx & z1 \notin p2].
   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 Lp]]; first by exists nil.
-rewrite inE => /norP[ey'z1 /(IHp Lp){p Lp}{}IHp].
+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}].
diff --git a/theories/part.v b/theories/part.v
index b29fe36..54604c8 100644
--- a/theories/part.v
+++ b/theories/part.v
@@ -1226,7 +1226,7 @@ have{fit_p4}: let: (h23, q12) := conv_part12 p4 in
   by split; last by rewrite Dn Es1 Eh12 Ef21 Ef22 /inv_face2 !nodeK.
 case: {p4}(conv_part12 p4) => [h23 q12] [Eh23 fit_q12].
 move: (drop_part 5 p1) (size_drop_part 5 p1) (fitp_drop 5 fit_p1) => p6 Ep6.
-have{Ep1}{}Ep6: arity x = 5 + size_part p6 by rewrite Ep6 -(eqP Ep1) subnKC.
+have{Ep1}Ep6: arity x = 5 + size_part p6 by rewrite Ep6 -(eqP Ep1) subnKC.
 move=> /= fit_p6.
 rewrite -2!arity_face {1}/inv_face2 !nodeK Eu /=; apply: {q12}fit_q12.
 case: p6 fit_p6 Ep6 => //= [_ Ex5 | f31 _ p7 /and3P[Ef31 _]].
diff --git a/theories/present.v b/theories/present.v
index 985e46c..6eda30c 100644
--- a/theories/present.v
+++ b/theories/present.v
@@ -122,7 +122,7 @@ have p0lpl: forced_part p0l pl.
   rewrite /p0l; case: ifP => [p0ijk | _] G x x_ok //.
   by rewrite !fitp_split // => /andP[-> /p0p->].
 have {}pl_ok: successful pl by apply: pl_ok.
-have{p0lpl}{}pr_ok: successful pr.
+have{p0lpl}pr_ok: successful pr.
   apply: pr_ok => G x x_ok => [|p0x]; have:= pl_ok G x x_ok.
     exact/contra/p0lpl.
   by rewrite !fitp_split // p0p ?andbT ?addNb.

From e8dc6293e15d64e4b1832f4d8f7455a15e451a10 Mon Sep 17 00:00:00 2001
From: Yves Bertot <Yves.Bertot@inria.fr>
Date: Mon, 28 Mar 2022 16:49:35 +0200
Subject: [PATCH 4/5] 2 remaining duplicate clear, and silence other warnings
 in _CoqProject

---
 _CoqProject      | 8 ++++++++
 theories/embed.v | 2 +-
 theories/kempe.v | 2 +-
 3 files changed, 10 insertions(+), 2 deletions(-)

diff --git a/_CoqProject b/_CoqProject
index e535e4b..cbee69f 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -120,3 +120,11 @@ theories/unavoidability.v
 theories/reducibility.v
 theories/combinatorial4ct.v
 theories/fourcolor.v
+
+-R theories fourcolor
+-arg -w -arg -notation-overridden
+-arg -w -arg -ambiguous-paths
+-arg -w -arg -redundant-canonical-projection
+-arg -w -arg -deprecated-hint-without-locality
+-arg -w -arg -deprecated-instance-without-locality
+
diff --git a/theories/embed.v b/theories/embed.v
index c020be8..e767730 100644
--- a/theories/embed.v
+++ b/theories/embed.v
@@ -1376,7 +1376,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 *.
diff --git a/theories/kempe.v b/theories/kempe.v
index fe02455..90a4e61 100644
--- a/theories/kempe.v
+++ b/theories/kempe.v
@@ -198,7 +198,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 [].

From 224fde601dce61889deac8879a11ae75c52b7d25 Mon Sep 17 00:00:00 2001
From: Yves Bertot <Yves.Bertot@inria.fr>
Date: Mon, 28 Mar 2022 22:59:23 +0200
Subject: [PATCH 5/5] fix order of directives

---
 _CoqProject | 11 ++++-------
 1 file changed, 4 insertions(+), 7 deletions(-)

diff --git a/_CoqProject b/_CoqProject
index cbee69f..5a492fe 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,6 +1,10 @@
 -R theories fourcolor
 -arg -w -arg -notation-overridden
+-arg -w -arg -ambiguous-paths
 -arg -w -arg -redundant-canonical-projection
+-arg -w -arg -deprecated-hint-without-locality
+-arg -w -arg -deprecated-instance-without-locality
+
 theories/real.v
 theories/realsyntax.v
 theories/realprop.v
@@ -121,10 +125,3 @@ theories/reducibility.v
 theories/combinatorial4ct.v
 theories/fourcolor.v
 
--R theories fourcolor
--arg -w -arg -notation-overridden
--arg -w -arg -ambiguous-paths
--arg -w -arg -redundant-canonical-projection
--arg -w -arg -deprecated-hint-without-locality
--arg -w -arg -deprecated-instance-without-locality
-