Merge pull request #66 from CohenCyril/mc1300

Another way to adapt to math-comp#1300
coq-community · Jan 23, 2025 · 2cd48e2 · 2cd48e2
2 parents 1739214 + 595c624
commit 2cd48e2
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.