diff --git a/theories/proof/coloring.v b/theories/proof/coloring.v
index 13e01d5..db895fa 100644
--- a/theories/proof/coloring.v
+++ b/theories/proof/coloring.v
@@ -263,7 +263,7 @@ have oE_G'' w: order edge w = #|predD1 (cedge (h'' w)) unx|.
   have [u_nx | nx'u] := altP eqP.
     by apply/imageP => [[wu _ u_wu]]; case/eqP: (valP wu); rewrite -[RHS]u_nx.
   set wu : G'' := Sub u nx'u; rewrite (mem_image Ih'' _ wu) /=.
-  apply: etrans (eq_fconnect (glink_fp_skip_edge _) w wu) _.
+  apply: etrans (@eq_fconnect _ _ _ (glink_fp_skip_edge _) w wu) _.
     by rewrite /glink /= -!val_eqE /= nnx !eqxx /= orbT.
   exact: (fconnect_skip edgeI w wu).
 have [|k [kE kF]] := minimal_counter_example_is_minimal cexG _ ltG''G.
diff --git a/theories/proof/discharge.v b/theories/proof/discharge.v
index e62f78a..0087e68 100644
--- a/theories/proof/discharge.v
+++ b/theories/proof/discharge.v
@@ -217,7 +217,7 @@ Qed.
 
 Lemma dscore_mirror (x : G) : @dscore (mirror G) x = dscore x.
 Proof.
-rewrite /dscore arity_mirror (eq_bigl _ _ (cface_mirror x)); congr (_ + _).
+rewrite /dscore arity_mirror (eq_bigl _ _ (@cface_mirror _ x)); congr (_ + _).
 suffices{x} score1F (x : G): @dscore1 (mirror G) (face x) = dscore1 x.
   rewrite (reindex_inj (@faceI G)) -(eq_bigl _ _ (fun y => cface1r y x)) /=.
   by apply: eq_bigr => y _; rewrite /dscore2 2!{1}score1F (plain_eq' geoG).
diff --git a/theories/proof/geometry.v b/theories/proof/geometry.v
index 114ad9a..65e4639 100644
--- a/theories/proof/geometry.v
+++ b/theories/proof/geometry.v
@@ -158,7 +158,7 @@ Lemma iter_face_subn n x :
 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.
+Proof. by move=> x; apply/eq_card/(@cface_mirror _ x). Qed.
 
 Section SimplePaths.