From 1e13238bcabdff52bef47f8867e221ce12d0c92b Mon Sep 17 00:00:00 2001
From: Jan-Oliver Kaiser <janno@bedrocksystems.com>
Date: Wed, 20 Nov 2024 17:10:38 +0100
Subject: [PATCH] Support export locality in `coq.TC.declare-instance`.

Also add and fix tests for the primitive.
---
 src/coq_elpi_builtins.ml |  2 +-
 tests/test_API_TC_CS.v   | 26 ++++++++++++++++++++++----
 2 files changed, 23 insertions(+), 5 deletions(-)

diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
index 1027e3df4..7f4aa02aa 100644
--- a/src/coq_elpi_builtins.ml
+++ b/src/coq_elpi_builtins.ml
@@ -2781,7 +2781,7 @@ Supported attributes:
 Supported attributes:
 - @global! (default: true)|}))),
   (fun gr priority ~depth { options } _ -> grab_global_env "coq.TC.declare-instance" (fun state ->
-     let global = if options.local = Some false then Hints.SuperGlobal else Hints.Local in
+     let global = hint_locality options in
      let hint_priority = Some priority in
      Classes.existing_instance global gr
           (Some { Hints.empty_hint_info with Typeclasses.hint_priority });
diff --git a/tests/test_API_TC_CS.v b/tests/test_API_TC_CS.v
index ac45723e2..7a2cbd2a0 100644
--- a/tests/test_API_TC_CS.v
+++ b/tests/test_API_TC_CS.v
@@ -15,11 +15,29 @@ Proof.
 exact Rr.
 Defined.
 
-Check (_ : Reflexive R).
+Fail Example ex : Reflexive R := _.
+
+Module TCLocal.
+  Elpi Query lp:{{ coq.locate "myi" GR, @local! => coq.TC.declare-instance GR 10. }}.
+  Succeed Example ex : Reflexive R := _.
+End TCLocal.
+
+Module TCExport.
+  Fail Example ex : Reflexive R := _.
+  Module Mod.
+    Elpi Query lp:{{ coq.locate "myi" GR, coq.TC.declare-instance GR 10. }}.
+  End Mod.
+  Fail Example ex : Reflexive R := _.
+  Import Mod.
+  Check (_ : Reflexive R).
+  Succeed Example ex : Reflexive R := _.
+End TCExport.
+
+Module TCGlobal.
+  Elpi Query lp:{{ coq.locate "myi" GR, @global! => coq.TC.declare-instance GR 10. }}.
+End TCGlobal.
+Succeed Example ex : Reflexive R := _.
 
-Elpi Query lp:{{coq.locate "myi" GR, coq.TC.declare-instance GR 10. }}.
-
-Check (_ : Reflexive R).
 
 Elpi Query lp:{{coq.TC.db L}}.
 Elpi Query lp:{{coq.locate "RewriteRelation" GR, coq.TC.db-for GR L}}.