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