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.

4 files changed, 12 insertions, 10 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index ee27a9f58b..99c92604ba 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -29,8 +29,8 @@ module NamedDecl = Context.Named.Declaration
 (*i*)
 
 let set_typeclass_transparency c local b =
-  let superglobal = true in
-  Hints.add_hints ~local ~superglobal [typeclasses_db]
+  let locality = if local then Goptions.OptLocal else Goptions.OptGlobal in
+  Hints.add_hints ~locality [typeclasses_db]
     (Hints.HintsTransparencyEntry (Hints.HintsReferences [c], b))
 
 let classes_transparent_state () =
@@ -41,9 +41,9 @@ let classes_transparent_state () =
 let () =
   Hook.set Typeclasses.classes_transparent_state_hook classes_transparent_state
 
-let add_instance_hint inst path ~local ~superglobal info poly =
+let add_instance_hint inst path ~locality info poly =
      Flags.silently (fun () ->
-       Hints.add_hints ~local ~superglobal [typeclasses_db]
+       Hints.add_hints ~locality [typeclasses_db]
           (Hints.HintsResolveEntry
              [info, poly, false, Hints.PathHints path, inst])) ()
 
@@ -57,13 +57,13 @@ let is_local_for_hint i =
 
 let add_instance_base inst =
   let poly = Global.is_polymorphic inst.is_impl in
-  let local = is_local_for_hint inst in
-  add_instance_hint (Hints.IsGlobRef inst.is_impl) [inst.is_impl] ~local ~superglobal:true
+  let locality = if is_local_for_hint inst then Goptions.OptLocal else Goptions.OptGlobal in
+  add_instance_hint (Hints.IsGlobRef inst.is_impl) [inst.is_impl] ~locality
     inst.is_info poly;
   List.iter (fun (path, pri, c) ->
     let h = Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty) [@ocaml.warning "-3"] in
     add_instance_hint h path
-                ~local ~superglobal:true pri poly)
+                ~locality pri poly)
     (build_subclasses ~check:(not (isVarRef inst.is_impl))
        (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_info)
 
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index 527c6e24c8..c973c84827 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -123,7 +123,8 @@ let shrink_body c ty =
 let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst]
 
 let add_hint local prg cst =
-  Hints.add_hints ~local ~superglobal:false [Id.to_string prg.prg_name] (unfold_entry cst)
+  let locality = if local then Goptions.OptLocal else Goptions.OptExport in
+  Hints.add_hints ~locality [Id.to_string prg.prg_name] (unfold_entry cst)
 
 (***********************************************************************)
 (* Saving an obligation                                                *)
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 7ce2d2a49c..dd90af0223 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -296,7 +296,7 @@ open Evd
 let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst]
 
 let add_local_hint prg cst =
-  Hints.add_hints ~local:true ~superglobal:false [Id.to_string prg.prg_name] (unfold_entry cst)
+  Hints.add_hints ~locality:Goptions.OptLocal [Id.to_string prg.prg_name] (unfold_entry cst)
 
 let init_prog_info ?(opaque = false) ?hook n udecl b t ctx deps fixkind
                    notations obls impls ~scope ~poly ~kind reduce =
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index be6ffa07b9..c4027c6598 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1180,7 +1180,8 @@ let vernac_hints ~atts dbnames h =
   in
   let local, poly = Attributes.(parse Notations.(locality ++ polymorphic) atts) in
   let local = enforce_module_locality local in
-  Hints.add_hints ~local ~superglobal:true dbnames (Hints.interp_hints ~poly h)
+  let locality = if local then OptLocal else OptGlobal in
+  Hints.add_hints ~locality dbnames (Hints.interp_hints ~poly h)
 
 let vernac_syntactic_definition ~atts lid x only_parsing =
   let module_local, deprecation = Attributes.(parse Notations.(module_locality ++ deprecation) atts) in