From 245b94cd075b6be527590c425a98262d89577909 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 11 Mar 2020 11:29:40 +0100
Subject: Hack a non-superglobal mode for hints.

The current implementation was seemingly never thought for this kind of
semantics. Everything is superglobal by construction, notably hint database
creation and naming schemes. The new mode feels a bit hackish to me, at
some point this should be fully reimplemented from scratch with a clear
design in mind.
---
 plugins/ltac/g_auto.mlg | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 82c64a9857..336c5a4bb0 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -249,7 +249,7 @@ 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
-        Hints.add_hints ~local:(Locality.make_section_locality locality)
+        Hints.add_hints ~local:(Locality.make_section_locality locality) ~superglobal:true
           (match dbnames with None -> ["core"] | Some l -> l) entry;
  }
 END
-- 
cgit v1.2.3


From 96ec58df041dc0111df0e681269aed9d0e9b571a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 12 Mar 2020 15:11:35 +0100
Subject: Use a 3-valued flag for hint locality.

We reuse the same type as for options, even though it is a bit ill-named. At
least it allows to share code with it.
---
 plugins/ltac/g_auto.mlg | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 336c5a4bb0..c43018022e 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -249,7 +249,8 @@ 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
-        Hints.add_hints ~local:(Locality.make_section_locality locality) ~superglobal:true
+        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;
  }
 END
-- 
cgit v1.2.3