From 91a5b23645b508204d392d3e129a2b9b4588ca64 Mon Sep 17 00:00:00 2001
From: Florent Hivert <Florent.Hivert@lri.fr>
Date: Wed, 31 Jan 2024 09:59:41 +0100
Subject: [PATCH] Added #[export] to Hint resolve

---
 theories/Combi/setpartition.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Combi/setpartition.v b/theories/Combi/setpartition.v
index a5f3271..b1db52e 100644
--- a/theories/Combi/setpartition.v
+++ b/theories/Combi/setpartition.v
@@ -179,7 +179,7 @@ by apply/set0Pn; exists x.
 Qed.
 
 End Defs.
-Hint Resolve setpartP trivIsetpart setpart_non0 : core.
+#[export] Hint Resolve setpartP trivIsetpart setpart_non0 : core.
 
 
 Section Empty.