Export the user-facing attribute for hint locality.

5 files changed, 60 insertions, 9 deletions

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 7cde342662..9c0cf03854 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1189,6 +1189,12 @@ let remove_hints local dbnames grs =
 (**************************************************************************)
 (*                     The "Hint" vernacular command                      *)
 (**************************************************************************)
+
+let check_no_export ~local ~superglobal () =
+  (* TODO: implement export for these entries *)
+  if not local && not superglobal then
+    CErrors.user_err Pp.(str "This command does not support the \"export\" attribute")
+
 let add_resolves env sigma clist ~local ~superglobal dbnames =
   List.iter
     (fun dbname ->
@@ -1208,14 +1214,16 @@ let add_unfolds l ~local ~superglobal dbnames =
       Lib.add_anonymous_leaf (inAutoHint hint))
     dbnames
 
-let add_cuts l local dbnames =
+let add_cuts l ~local ~superglobal dbnames =
+  let () = check_no_export ~local ~superglobal () in
   List.iter
     (fun dbname ->
       let hint = make_hint ~local dbname (AddCut l) in
       Lib.add_anonymous_leaf (inAutoHint hint))
     dbnames
 
-let add_mode l m local dbnames =
+let add_mode l m ~local ~superglobal dbnames =
+  let () = check_no_export ~local ~superglobal () in
   List.iter
     (fun dbname ->
       let m' = make_mode l m in
@@ -1223,7 +1231,8 @@ let add_mode l m local dbnames =
       Lib.add_anonymous_leaf (inAutoHint hint))
     dbnames
 
-let add_transparency l b local dbnames =
+let add_transparency l b ~local ~superglobal dbnames =
+  let () = check_no_export ~local ~superglobal () in
   List.iter
     (fun dbname ->
       let hint = make_hint ~local dbname (AddTransparency (l, b)) in
@@ -1424,11 +1433,11 @@ let add_hints ~locality dbnames h =
   match h with
   | HintsResolveEntry lhints -> add_resolves env sigma lhints ~local ~superglobal dbnames
   | HintsImmediateEntry lhints -> add_trivials env sigma lhints ~local ~superglobal dbnames
-  | HintsCutEntry lhints -> add_cuts lhints local dbnames
-  | HintsModeEntry (l,m) -> add_mode l m local dbnames
+  | HintsCutEntry lhints -> add_cuts lhints ~local ~superglobal dbnames
+  | HintsModeEntry (l,m) -> add_mode l m ~local ~superglobal dbnames
   | HintsUnfoldEntry lhints -> add_unfolds lhints ~local ~superglobal dbnames
   | HintsTransparencyEntry (lhints, b) ->
-      add_transparency lhints b local dbnames
+      add_transparency lhints b ~local ~superglobal dbnames
   | HintsExternEntry (info, tacexp) ->
       add_externs info tacexp ~local ~superglobal dbnames
 
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.
diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index 7213ba4829..96f126503d 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -163,6 +163,16 @@ let program =
 
 let locality = bool_attribute ~name:"Locality" ~on:"local" ~off:"global"
 
+let option_locality =
+  let name = "Locality" in
+  attribute_of_list [
+    ("local", single_key_parser ~name ~key:"local" Goptions.OptLocal);
+    ("global", single_key_parser ~name ~key:"global" Goptions.OptGlobal);
+    ("export", single_key_parser ~name ~key:"export" Goptions.OptExport);
+  ] >>= function
+  | None -> return Goptions.OptDefault
+  | Some l -> return l
+
 let ukey = "universes"
 
 let universe_polymorphism_option_name = ["Universe"; "Polymorphism"]
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index 7ecb7e4fb0..660652081f 100644
--- a/vernac/attributes.mli
+++ b/vernac/attributes.mli
@@ -47,6 +47,7 @@ val polymorphic : bool attribute
 val program : bool attribute
 val template : bool option attribute
 val locality : bool option attribute
+val option_locality : Goptions.option_locality attribute
 val deprecation : Deprecation.t option attribute
 val canonical_field : bool attribute
 val canonical_instance : bool attribute
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index c4027c6598..ba6d869589 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1178,9 +1178,18 @@ let vernac_hints ~atts dbnames h =
       (warn_implicit_core_hint_db (); ["core"])
     else dbnames
   in
-  let local, poly = Attributes.(parse Notations.(locality ++ polymorphic) atts) in
-  let local = enforce_module_locality local in
-  let locality = if local then OptLocal else OptGlobal in
+  let locality, poly = Attributes.(parse Notations.(option_locality ++ polymorphic) atts) in
+  let () = match locality with
+  | OptGlobal ->
+    if Global.sections_are_opened () then
+    CErrors.user_err Pp.(str
+      "This command does not support the global attribute in sections.");
+  | OptExport ->
+    if Global.sections_are_opened () then
+    CErrors.user_err Pp.(str
+      "This command does not support the export attribute in sections.");
+  | OptDefault | OptLocal -> ()
+  in
   Hints.add_hints ~locality dbnames (Hints.interp_hints ~poly h)
 
 let vernac_syntactic_definition ~atts lid x only_parsing =