Merge pull request #715 from Janno/janno/declare-instance-export-upstream

Support export locality in `coq.TC.declare-instance`.

Author: gares

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 });

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}}.