From 623fc72ae32a3ed6bc8be9fed8e46f83c006bde9 Mon Sep 17 00:00:00 2001
From: Quentin Vermande <quentin.vermande@orange.fr>
Date: Wed, 27 Nov 2024 17:16:33 +0100
Subject: [PATCH] restore `cface_mirror`'s implicit arguments

---
 theories/proof/hypermap.v | 2 ++
 1 file changed, 2 insertions(+)

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.