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.

1 files changed, 6 insertions, 1 deletions

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));