From 082ec7c44f39f25bc3e59524dd9b358f1a209bca Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@lri.fr>
Date: Mon, 7 Jun 2021 14:41:54 +0200
Subject: All tests go through

---
 src/QInst.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/QInst.v b/src/QInst.v
index e78a2fe..41da06b 100644
--- a/src/QInst.v
+++ b/src/QInst.v
@@ -27,7 +27,7 @@ Proof.
    installed when we compile SMTCoq. *)
 Qed.
 
-#[export] Hint Resolve impl_split : smtcoq_core.
+#[global] Hint Resolve impl_split : smtcoq_core.
 
 (** verit silently transforms an <implb (a || b) c> into a <or (not a) c>
    or into a <or (not b) c> when instantiating such a quantified theorem *)
-- 
cgit