Merge PR #13388: Export locality for all hint commands

Reviewed-by: silene
Reviewed-by: gares
Reviewed-by: Zimmi48

1 files changed, 16 insertions, 5 deletions

diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 44472a1995..15861d49be 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -240,10 +240,21 @@ ARGUMENT EXTEND opthints
 END
 
 VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF
-| #[ locality = Attributes.locality; ] [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> {
-        let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in
-        let locality = if Locality.make_section_locality locality then Goptions.OptLocal else Goptions.OptGlobal in
-        Hints.add_hints ~locality
-          (match dbnames with None -> ["core"] | Some l -> l) entry;
+| #[ locality = Attributes.option_locality; ] [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> {
+  let open Goptions in
+  let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) 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
+    (match dbnames with None -> ["core"] | Some l -> l) entry;
  }
 END