2 remaining duplicate clear, and silence other warnings in _CoqProject

_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
+

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 *.

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 [].