update wrt math-comp#1300

coq-community · Dec 9, 2024 · 595c624 · 595c624
1 parent 1739214
commit 595c624
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.