From ae56bbe12270694a0cde96e343fa5f2ee9874f24 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 15 Nov 2020 14:25:35 +0100
Subject: Implement export locality for the remaining Hint commands.

---
 plugins/ltac/g_auto.mlg | 21 ++++++++++++++++-----
 1 file changed, 16 insertions(+), 5 deletions(-)

(limited to 'plugins')

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
-- 
cgit v1.2.3