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