diff options
| author | Pierre-Marie Pédrot | 2020-03-12 15:11:35 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-03-18 11:44:50 +0100 |
| commit | 96ec58df041dc0111df0e681269aed9d0e9b571a (patch) | |
| tree | 7abcbb4ec26dfd3fb2ac81934d6e8c8602cc7d80 /vernac/classes.ml | |
| parent | 245b94cd075b6be527590c425a98262d89577909 (diff) | |
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.
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 14 |
1 files changed, 7 insertions, 7 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) |