aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/ltac/g_auto.mlg2
-rw-r--r--pretyping/typeclasses.ml3
-rw-r--r--pretyping/typeclasses.mli3
-rw-r--r--tactics/hints.ml51
-rw-r--r--tactics/hints.mli2
-rw-r--r--vernac/classes.ml20
-rw-r--r--vernac/declareObl.ml2
-rw-r--r--vernac/obligations.ml6
-rw-r--r--vernac/record.ml2
-rw-r--r--vernac/vernacentries.ml2
10 files changed, 47 insertions, 46 deletions
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 82c64a9857..336c5a4bb0 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -249,7 +249,7 @@ 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)
+ Hints.add_hints ~local:(Locality.make_section_locality locality) ~superglobal:true
(match dbnames with None -> ["core"] | Some l -> l) entry;
}
END
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index aa2e96c2d7..d4f59d7a36 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -34,9 +34,6 @@ let get_typeclasses_unique_solutions =
~key:["Typeclasses";"Unique";"Solutions"]
~value:false
-let (set_typeclass_transparency, set_typeclass_transparency_hook) = Hook.make ()
-let set_typeclass_transparency gr local c = Hook.get set_typeclass_transparency gr local c
-
let (classes_transparent_state, classes_transparent_state_hook) = Hook.make ()
let classes_transparent_state () = Hook.get classes_transparent_state ()
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 2715c1eda5..c350f97107 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -122,9 +122,6 @@ val resolve_typeclasses : ?filter:evar_filter -> ?unique:bool ->
?split:bool -> ?fail:bool -> env -> evar_map -> evar_map
val resolve_one_typeclass : ?unique:bool -> env -> evar_map -> EConstr.types -> evar_map * EConstr.constr
-val set_typeclass_transparency_hook : (evaluable_global_reference -> bool (*local?*) -> bool -> unit) Hook.t
-val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> unit
-
val classes_transparent_state_hook : (unit -> TransparentState.t) Hook.t
val classes_transparent_state : unit -> TransparentState.t
diff --git a/tactics/hints.ml b/tactics/hints.ml
index e9ed43e3de..8b81b36fa2 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1031,7 +1031,7 @@ let remove_hint dbname grs =
type hint_action =
| CreateDB of bool * TransparentState.t
| AddTransparency of evaluable_global_reference hints_transparency_target * bool
- | AddHints of hint_entry list
+ | AddHints of { superglobal : bool; hints : hint_entry list }
| RemoveHints of GlobRef.t list
| AddCut of hints_path
| AddMode of GlobRef.t * hint_mode array
@@ -1057,14 +1057,21 @@ let load_autohint _ (kn, h) =
match h.hint_action with
| CreateDB (b, st) -> searchtable_add (name, Hint_db.empty ~name st b)
| AddTransparency (grs, b) -> add_transparency name grs b
- | AddHints hints -> add_hint name hints
+ | AddHints { superglobal; hints } ->
+ if superglobal then add_hint name hints
| RemoveHints grs -> remove_hint name grs
| AddCut path -> add_cut name path
| AddMode (l, m) -> add_mode name l m
let open_autohint i (kn, h) =
if Int.equal i 1 then match h.hint_action with
- | AddHints hints ->
+ | AddHints { superglobal; hints } ->
+ let () =
+ if not superglobal then
+ (* Import-bound hints must be declared when not imported yet *)
+ let filter (_, h) = not @@ KNmap.mem h.code.uid !statustable in
+ add_hint h.hint_name (List.filter filter hints)
+ in
let add (_, hint) = statustable := KNmap.add hint.code.uid true !statustable in
List.iter add hints
| _ -> ()
@@ -1133,9 +1140,9 @@ let subst_autohint (subst, obj) =
else HintsReferences grs'
in
if target' == target then obj.hint_action else AddTransparency (target', b)
- | AddHints hintlist ->
- let hintlist' = List.Smart.map subst_hint hintlist in
- if hintlist' == hintlist then obj.hint_action else AddHints hintlist'
+ | AddHints { superglobal; hints } ->
+ let hints' = List.Smart.map subst_hint hints in
+ if hints' == hints then obj.hint_action else AddHints { superglobal; hints = hints' }
| RemoveHints grs ->
let grs' = List.Smart.map (subst_global_reference subst) grs in
if grs == grs' then obj.hint_action else RemoveHints grs'
@@ -1150,7 +1157,7 @@ let subst_autohint (subst, obj) =
let classify_autohint obj =
match obj.hint_action with
- | AddHints [] -> Dispose
+ | AddHints { hints = [] } -> Dispose
| _ -> if obj.hint_local then Dispose else Substitute obj
let inAutoHint : hint_obj -> obj =
@@ -1182,7 +1189,7 @@ let remove_hints local dbnames grs =
(**************************************************************************)
(* The "Hint" vernacular command *)
(**************************************************************************)
-let add_resolves env sigma clist local dbnames =
+let add_resolves env sigma clist ~local ~superglobal dbnames =
List.iter
(fun dbname ->
let r =
@@ -1190,14 +1197,14 @@ let add_resolves env sigma clist local dbnames =
make_resolves env sigma (true,hnf,not !Flags.quiet)
pri ~poly ~name:path gr) clist)
in
- let hint = make_hint ~local dbname (AddHints r) in
+ let hint = make_hint ~local dbname (AddHints { superglobal; hints = r }) in
Lib.add_anonymous_leaf (inAutoHint hint))
dbnames
-let add_unfolds l local dbnames =
+let add_unfolds l ~local ~superglobal dbnames =
List.iter
(fun dbname ->
- let hint = make_hint ~local dbname (AddHints (List.map make_unfold l)) in
+ let hint = make_hint ~local dbname (AddHints { superglobal; hints = List.map make_unfold l }) in
Lib.add_anonymous_leaf (inAutoHint hint))
dbnames
@@ -1223,23 +1230,23 @@ let add_transparency l b local dbnames =
Lib.add_anonymous_leaf (inAutoHint hint))
dbnames
-let add_extern info tacast local dbname =
+let add_extern info tacast ~local ~superglobal dbname =
let pat = match info.hint_pattern with
| None -> None
| Some (_, pat) -> Some pat
in
let hint = make_hint ~local dbname
- (AddHints [make_extern (Option.get info.hint_priority) pat tacast]) in
+ (AddHints { superglobal; hints = [make_extern (Option.get info.hint_priority) pat tacast] }) in
Lib.add_anonymous_leaf (inAutoHint hint)
-let add_externs info tacast local dbnames =
- List.iter (add_extern info tacast local) dbnames
+let add_externs info tacast ~local ~superglobal dbnames =
+ List.iter (add_extern info tacast ~local ~superglobal) dbnames
-let add_trivials env sigma l local dbnames =
+let add_trivials env sigma l ~local ~superglobal dbnames =
List.iter
(fun dbname ->
let l = List.map (fun (name, poly, c) -> make_trivial env sigma poly ~name c) l in
- let hint = make_hint ~local dbname (AddHints l) in
+ let hint = make_hint ~local dbname (AddHints { superglobal; hints = l }) in
Lib.add_anonymous_leaf (inAutoHint hint))
dbnames
@@ -1403,22 +1410,22 @@ 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 dbnames h =
+let add_hints ~local ~superglobal dbnames h =
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));
let env = Global.env() in
let sigma = Evd.from_env env in
match h with
- | HintsResolveEntry lhints -> add_resolves env sigma lhints local dbnames
- | HintsImmediateEntry lhints -> add_trivials env sigma lhints local dbnames
+ | HintsResolveEntry lhints -> add_resolves env sigma lhints ~local ~superglobal dbnames
+ | HintsImmediateEntry lhints -> add_trivials env sigma lhints ~local ~superglobal dbnames
| HintsCutEntry lhints -> add_cuts lhints local dbnames
| HintsModeEntry (l,m) -> add_mode l m local dbnames
- | HintsUnfoldEntry lhints -> add_unfolds lhints local dbnames
+ | HintsUnfoldEntry lhints -> add_unfolds lhints ~local ~superglobal dbnames
| HintsTransparencyEntry (lhints, b) ->
add_transparency lhints b local dbnames
| HintsExternEntry (info, tacexp) ->
- add_externs info tacexp local dbnames
+ add_externs info tacexp ~local ~superglobal dbnames
let expand_constructor_hints env sigma lems =
List.map_append (fun (evd,lem) ->
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 2663f65851..3fd4d6ea9e 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 -> hint_db_name list -> hints_entry -> unit
+val add_hints : local:bool -> superglobal:bool -> 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 16b9e07fb2..ee27a9f58b 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -29,7 +29,8 @@ module NamedDecl = Context.Named.Declaration
(*i*)
let set_typeclass_transparency c local b =
- Hints.add_hints ~local [typeclasses_db]
+ let superglobal = true in
+ Hints.add_hints ~local ~superglobal [typeclasses_db]
(Hints.HintsTransparencyEntry (Hints.HintsReferences [c], b))
let classes_transparent_state () =
@@ -38,12 +39,11 @@ let classes_transparent_state () =
with Not_found -> TransparentState.empty
let () =
- Hook.set Typeclasses.set_typeclass_transparency_hook set_typeclass_transparency;
Hook.set Typeclasses.classes_transparent_state_hook classes_transparent_state
-let add_instance_hint inst path local info poly =
+let add_instance_hint inst path ~local ~superglobal info poly =
Flags.silently (fun () ->
- Hints.add_hints ~local [typeclasses_db]
+ Hints.add_hints ~local ~superglobal [typeclasses_db]
(Hints.HintsResolveEntry
[info, poly, false, Hints.PathHints path, inst])) ()
@@ -55,16 +55,16 @@ let is_local_for_hint i =
add_instance_hint; don't ask hints to take discharge into account
itself *)
-let add_instance check inst =
+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
+ add_instance_hint (Hints.IsGlobRef inst.is_impl) [inst.is_impl] ~local ~superglobal:true
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 pri poly)
- (build_subclasses ~check:(check && not (isVarRef inst.is_impl))
+ ~local ~superglobal:true pri poly)
+ (build_subclasses ~check:(not (isVarRef inst.is_impl))
(Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_info)
let mk_instance cl info glob impl =
@@ -104,7 +104,7 @@ let discharge_instance (_, inst) =
let is_local i = (i.is_global == None)
let rebuild_instance inst =
- add_instance true inst;
+ add_instance_base inst;
inst
let classify_instance inst =
@@ -124,7 +124,7 @@ let instance_input : instance -> obj =
let add_instance i =
Lib.add_anonymous_leaf (instance_input i);
- add_instance true i
+ add_instance_base i
let warning_not_a_class =
let name = "not-a-class" in
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index eb9b896ec6..527c6e24c8 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -123,7 +123,7 @@ let shrink_body c ty =
let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst]
let add_hint local prg cst =
- Hints.add_hints ~local [Id.to_string prg.prg_name] (unfold_entry cst)
+ Hints.add_hints ~local ~superglobal:false [Id.to_string prg.prg_name] (unfold_entry cst)
(***********************************************************************)
(* Saving an obligation *)
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 27eb821a6a..7ce2d2a49c 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -295,8 +295,8 @@ open Evd
let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst]
-let add_hint local prg cst =
- Hints.add_hints ~local [Id.to_string prg.prg_name] (unfold_entry cst)
+let add_local_hint prg cst =
+ Hints.add_hints ~local:true ~superglobal:false [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 =
@@ -461,7 +461,7 @@ let obligation_hook prg obl num auto { DeclareDef.Hook.S.uctx = ctx'; dref; _ }
Univ.UContext.instance uctx, ctx'
in
let obl = { obl with obl_body = Some (DefinedObl (cst, inst)) } in
- let () = if transparent then add_hint true prg cst in
+ let () = if transparent then add_local_hint prg cst in
let obls = Array.copy obls in
let () = obls.(num) <- obl in
let prg = { prg with prg_ctx = ctx' } in
diff --git a/vernac/record.ml b/vernac/record.ml
index 065641989d..75e1088108 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -613,7 +613,7 @@ let add_constant_class env sigma cst =
}
in
Classes.add_class env sigma tc;
- set_typeclass_transparency (EvalConstRef cst) false false
+ Classes.set_typeclass_transparency (EvalConstRef cst) false false
let add_inductive_class env sigma ind =
let mind, oneind = Inductive.lookup_mind_specif env ind in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index c78b470e3b..be6ffa07b9 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1180,7 +1180,7 @@ 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 dbnames (Hints.interp_hints ~poly h)
+ Hints.add_hints ~local ~superglobal:true 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-11 02:05:22 +0000