adapt to mc#1300

coq-community · Dec 9, 2024 · a8bf4e0 · a8bf4e0
1 parent 957fd92
commit a8bf4e0
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/theories/proof/hypermap.v b/theories/proof/hypermap.v
@@ -429,6 +429,8 @@ by rewrite -(mem2_last x) !rev_cons last_cat !last_rcons mem2_cat => ->.
 Qed.
 
 End DerivedMaps.
+Arguments cface_mirror [G].
+Arguments cnode_mirror [G].
 
 Section EqualHypermap.