restore cface_mirror's implicit arguments

coq-community · Jan 7, 2025 · 623fc72 · 623fc72
1 parent 1739214
commit 623fc72
Showing 1 changed file with 2 additions and 0 deletions.
diff --git 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.