diff options
| -rw-r--r-- | plugins/ltac/g_auto.mlg | 3 | ||||
| -rw-r--r-- | tactics/hints.ml | 7 | ||||
| -rw-r--r-- | tactics/hints.mli | 2 | ||||
| -rw-r--r-- | vernac/classes.ml | 14 | ||||
| -rw-r--r-- | vernac/declareObl.ml | 3 | ||||
| -rw-r--r-- | vernac/obligations.ml | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 3 |
7 files changed, 21 insertions, 13 deletions
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 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) 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 |