diff --git a/theories/proof/hypermap.v b/theories/proof/hypermap.v
index 67741c2..37fd360 100644
--- a/theories/proof/hypermap.v
+++ b/theories/proof/hypermap.v
@@ -430,6 +430,8 @@ Qed.
 
 End DerivedMaps.
 
+Arguments cface_mirror [G] x y.
+
 Section EqualHypermap.
 
 Variable G : hypermap.