Merge PR #11812: Add an Export locality to hints

Reviewed-by: Zimmi48
Ack-by: gares
Ack-by: maximedenes

1 files changed, 22 insertions, 0 deletions

diff --git a/test-suite/success/export_hint.v b/test-suite/success/export_hint.v
new file mode 100644
index 0000000000..e18f7c1bef
--- /dev/null
+++ b/test-suite/success/export_hint.v
@@ -0,0 +1,22 @@
+Create HintDb foo.
+
+Module Foo.
+
+Axiom F : False.
+
+#[export]
+Hint Immediate F : foo.
+
+End Foo.
+
+Goal False.
+Proof.
+Fail solve [auto with foo].
+Abort.
+
+Import Foo.
+
+Goal False.
+Proof.
+auto with foo.
+Qed.