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.
---
 tactics/hints.ml  | 7 ++++++-
 tactics/hints.mli | 2 +-
 2 files changed, 7 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 8b81b36fa2..7cde342662 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1410,7 +1410,12 @@ let interp_hints ~poly =
       let _, tacexp = Genintern.generic_intern env tacexp in
       HintsExternEntry ({ hint_priority = Some pri; hint_pattern = pat }, tacexp)
 
-let add_hints ~local ~superglobal dbnames h =
+let add_hints ~locality dbnames h =
+  let local, superglobal = match locality with
+  | Goptions.OptDefault | Goptions.OptGlobal -> false, true
+  | Goptions.OptExport -> false, false
+  | Goptions.OptLocal -> true, false
+  in
   if String.List.mem "nocore" dbnames then
     user_err Pp.(str "The hint database \"nocore\" is meant to stay empty.");
   assert (not (List.is_empty dbnames));
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 3fd4d6ea9e..c9d4231d77 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -219,7 +219,7 @@ val current_pure_db : unit -> hint_db list
 
 val interp_hints : poly:bool -> hints_expr -> hints_entry
 
-val add_hints : local:bool -> superglobal:bool -> hint_db_name list -> hints_entry -> unit
+val add_hints : locality:Goptions.option_locality -> hint_db_name list -> hints_entry -> unit
 
 val prepare_hint : bool (* Check no remaining evars *) ->
   env -> evar_map -> evar_map * constr -> (constr * Univ.ContextSet.t)
-- 
cgit v1.2.3