aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/ci/user-overlays/09567-ejgallego-hooks_unify.sh12
-rw-r--r--doc/plugin_tutorial/tuto1/src/simple_declare.ml9
-rw-r--r--plugins/funind/functional_principles_types.ml9
-rw-r--r--plugins/funind/indfun_common.ml4
-rw-r--r--plugins/funind/indfun_common.mli9
-rw-r--r--plugins/funind/recdef.ml4
-rw-r--r--plugins/ltac/rewrite.ml2
-rw-r--r--vernac/class.ml4
-rw-r--r--vernac/classes.ml6
-rw-r--r--vernac/comDefinition.ml40
-rw-r--r--vernac/comProgramFixpoint.ml4
-rw-r--r--vernac/declareDef.ml14
-rw-r--r--vernac/declareDef.mli28
-rw-r--r--vernac/lemmas.ml56
-rw-r--r--vernac/lemmas.mli38
-rw-r--r--vernac/obligations.ml60
-rw-r--r--vernac/obligations.mli29
-rw-r--r--vernac/vernacentries.ml2
18 files changed, 174 insertions, 156 deletions
diff --git a/dev/ci/user-overlays/09567-ejgallego-hooks_unify.sh b/dev/ci/user-overlays/09567-ejgallego-hooks_unify.sh
new file mode 100644
index 0000000000..27ce9aca16
--- /dev/null
+++ b/dev/ci/user-overlays/09567-ejgallego-hooks_unify.sh
@@ -0,0 +1,12 @@
+if [ "$CI_PULL_REQUEST" = "9567" ] || [ "$CI_BRANCH" = "hooks_unify" ]; then
+
+ equations_CI_REF=hooks_unify
+ equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+ mtac2_CI_REF=hooks_unify
+ mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
+
+ paramcoq_CI_REF=hooks_unify
+ paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq
+
+fi
diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
index 9d10a8ba72..e370d37fc4 100644
--- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml
+++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
@@ -1,5 +1,5 @@
(* Ideally coq/coq#8811 would get merged and then this function could be much simpler. *)
-let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook =
+let edeclare ?hook ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps =
let sigma = Evd.minimize_universes sigma in
let body = EConstr.to_constr sigma body in
let tyopt = Option.map (EConstr.to_constr sigma) tyopt in
@@ -9,16 +9,17 @@ let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook =
(Option.List.cons tyopt [body]) in
let sigma = Evd.restrict_universe_context sigma uvars in
let univs = Evd.check_univ_decl ~poly sigma udecl in
+ let uctx = Evd.evar_universe_context sigma in
let ubinders = Evd.universe_binders sigma in
let ce = Declare.definition_entry ?types:tyopt ~univs body in
- DeclareDef.declare_definition ident k ce ubinders imps ~hook
+ let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
+ DeclareDef.declare_definition ident k ce ubinders imps ?hook_data
let packed_declare_definition ~poly ident value_with_constraints =
let body, ctx = value_with_constraints in
let sigma = Evd.from_ctx ctx in
let k = (Decl_kinds.Global, poly, Decl_kinds.Definition) in
let udecl = UState.default_univ_decl in
- let nohook = Lemmas.mk_hook (fun _ x -> ()) in
- ignore (edeclare ident k ~opaque:false sigma udecl body None [] nohook)
+ ignore (edeclare ident k ~opaque:false sigma udecl body None [])
(* But this definition cannot be undone by Reset ident *)
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 25a7675113..ca09cad1f3 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -353,7 +353,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
in
let names = ref [new_princ_name] in
let hook =
- fun new_principle_type _ _ ->
+ fun new_principle_type _ _ _ _ ->
if Option.is_empty sorts
then
(* let id_of_f = Label.to_id (con_label f) in *)
@@ -385,7 +385,8 @@ let generate_functional_principle (evd: Evd.evar_map ref)
(* Pr 1278 :
Don't forget to close the goal if an error is raised !!!!
*)
- save false new_princ_name entry g_kind ~hook
+ let uctx = Evd.evar_universe_context sigma in
+ save false new_princ_name entry ~hook uctx g_kind
with e when CErrors.noncritical e ->
begin
begin
@@ -539,7 +540,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_
this_block_funs
0
(prove_princ_for_struct evd false 0 (Array.of_list (List.map fst funs)))
- (fun _ _ _ -> ())
+ (fun _ _ _ _ _ -> ())
with e when CErrors.noncritical e ->
begin
begin
@@ -614,7 +615,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_
this_block_funs
!i
(prove_princ_for_struct evd false !i (Array.of_list (List.map fst funs)))
- (fun _ _ _ -> ())
+ (fun _ _ _ _ _ -> ())
in
const
with Found_type i ->
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index f9938c0356..cba3cc3d42 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -129,7 +129,7 @@ let get_locality = function
| Local -> true
| Global -> false
-let save with_clean id const ?hook (locality,_,kind) =
+let save with_clean id const ?hook uctx (locality,_,kind) =
let fix_exn = Future.fix_exn_of const.const_entry_body in
let l,r = match locality with
| Discharge when Lib.sections_are_opened () ->
@@ -144,7 +144,7 @@ let save with_clean id const ?hook (locality,_,kind) =
(locality, ConstRef kn)
in
if with_clean then Proof_global.discard_current ();
- Lemmas.call_hook ?hook ~fix_exn l r;
+ Lemmas.call_hook ?hook ~fix_exn uctx [] l r;
definition_message id
let with_full_print f a =
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 9584649cff..1e0b95df34 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -42,7 +42,14 @@ val const_of_id: Id.t -> GlobRef.t(* constantyes *)
val jmeq : unit -> EConstr.constr
val jmeq_refl : unit -> EConstr.constr
-val save : bool -> Id.t -> Safe_typing.private_constants Entries.definition_entry -> ?hook:Lemmas.declaration_hook -> Decl_kinds.goal_kind -> unit
+val save
+ : bool
+ -> Id.t
+ -> Safe_typing.private_constants Entries.definition_entry
+ -> ?hook:Lemmas.declaration_hook
+ -> UState.t
+ -> Decl_kinds.goal_kind
+ -> unit
(* [with_full_print f a] applies [f] to [a] in full printing environment.
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index a8517e9ab1..8746c37309 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1310,7 +1310,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
let na = next_global_ident_away name Id.Set.empty in
if Termops.occur_existential sigma gls_type then
CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials");
- let hook _ _ =
+ let hook _ _ _ _ =
let opacity =
let na_ref = qualid_of_ident na in
let na_global = Smartlocate.global_with_alias na_ref in
@@ -1560,7 +1560,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
let tcc_lemma_name = add_suffix function_name "_tcc" in
let tcc_lemma_constr = ref Undefined in
(* let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *)
- let hook _ _ =
+ let hook _ _ _ _ =
let term_ref = Nametab.locate (qualid_of_ident term_id) in
let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in
let _ = Extraction_plugin.Table.extraction_inline true [qualid_of_ident term_id] in
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 7da4464e59..2d833a2cde 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1989,7 +1989,7 @@ let add_morphism_infer atts m n =
Decl_kinds.DefinitionBody Decl_kinds.Instance
in
let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
- let hook _ = function
+ let hook _ _ _ = function
| Globnames.ConstRef cst ->
add_instance (Typeclasses.new_instance
(Lazy.force PropGlobal.proper_class) Hints.empty_hint_info
diff --git a/vernac/class.ml b/vernac/class.ml
index 823177d4d1..a6b3242cae 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -302,7 +302,7 @@ let try_add_new_identity_coercion id ~local poly ~source ~target =
let try_add_new_coercion_with_source ref ~local poly ~source =
try_add_new_coercion_core ref ~local poly (Some source) None false
-let add_coercion_hook poly local ref =
+let add_coercion_hook poly _uctx _trans local ref =
let local = match local with
| Discharge
| Local -> true
@@ -314,7 +314,7 @@ let add_coercion_hook poly local ref =
let add_coercion_hook poly = Lemmas.mk_hook (add_coercion_hook poly)
-let add_subclass_hook poly local ref =
+let add_subclass_hook poly _uctx _trans local ref =
let stre = match local with
| Local -> true
| Global -> false
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 39c086eff5..263ebf5f5a 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -161,10 +161,10 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id
in obls, Some constr, typ
| None -> [||], None, termtype
in
- let univ_hook = Obligations.mk_univ_hook hook in
+ let hook = Lemmas.mk_hook hook in
let ctx = Evd.evar_universe_context sigma in
ignore (Obligations.add_definition id ?term:constr
- ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~univ_hook obls)
+ ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~hook obls)
else
Flags.silently (fun () ->
(* spiwack: it is hard to reorder the actions to do
@@ -175,7 +175,7 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id
let sigma = Evd.reset_future_goals sigma in
Lemmas.start_proof id ~pl:decl kind sigma (EConstr.of_constr termtype)
~hook:(Lemmas.mk_hook
- (fun _ -> instance_hook k pri global imps ?hook));
+ (fun _ _ _ -> instance_hook k pri global imps ?hook));
(* spiwack: I don't know what to do with the status here. *)
if not (Option.is_empty term) then
let init_refine =
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 5eb19eef54..28773a3965 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -94,22 +94,24 @@ let do_definition ~program_mode ?hook ident k univdecl bl red_option c ctypopt =
let (ce, evd, univdecl, imps as def) =
interp_definition ~program_mode univdecl bl (pi2 k) red_option c ctypopt
in
- if program_mode then
- let env = Global.env () in
- let (c,ctx), sideff = Future.force ce.const_entry_body in
- assert(Safe_typing.empty_private_constants = sideff);
- assert(Univ.ContextSet.is_empty ctx);
- let typ = match ce.const_entry_type with
- | Some t -> t
- | None -> EConstr.to_constr ~abort_on_undefined_evars:false evd (Retyping.get_type_of env evd (EConstr.of_constr c))
- in
- Obligations.check_evars env evd;
- let obls, _, c, cty =
- Obligations.eterm_obligations env ident evd 0 c typ
- in
- let ctx = Evd.evar_universe_context evd in
- let univ_hook = Obligations.mk_univ_hook (fun _ _ l r -> Lemmas.call_hook ?hook l r) in
- ignore(Obligations.add_definition
- ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ~univ_hook obls)
- else let ce = check_definition ~program_mode def in
- ignore(DeclareDef.declare_definition ident k ce (Evd.universe_binders evd) imps ?hook)
+ if program_mode then
+ let env = Global.env () in
+ let (c,ctx), sideff = Future.force ce.const_entry_body in
+ assert(Safe_typing.empty_private_constants = sideff);
+ assert(Univ.ContextSet.is_empty ctx);
+ let typ = match ce.const_entry_type with
+ | Some t -> t
+ | None -> EConstr.to_constr ~abort_on_undefined_evars:false evd (Retyping.get_type_of env evd (EConstr.of_constr c))
+ in
+ Obligations.check_evars env evd;
+ let obls, _, c, cty =
+ Obligations.eterm_obligations env ident evd 0 c typ
+ in
+ let ctx = Evd.evar_universe_context evd in
+ ignore(Obligations.add_definition
+ ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ?hook obls)
+ else
+ let ce = check_definition ~program_mode def in
+ let uctx = Evd.evar_universe_context evd in
+ let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
+ ignore(DeclareDef.declare_definition ident k ?hook_data ce (Evd.universe_binders evd) imps )
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index a30313d37c..cc9c83bd17 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -227,7 +227,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
in hook, recname, typ
in
(* XXX: Capturing sigma here... bad bad *)
- let univ_hook = Obligations.mk_univ_hook (hook sigma) in
+ let hook = Lemmas.mk_hook (hook sigma) in
(* XXX: Grounding non-ground terms here... bad bad *)
let fullcoqc = EConstr.to_constr ~abort_on_undefined_evars:false sigma def in
let fullctyp = EConstr.to_constr sigma typ in
@@ -237,7 +237,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
in
let ctx = Evd.evar_universe_context sigma in
ignore(Obligations.add_definition recname ~term:evars_def ~univdecl:decl
- evars_typ ctx evars ~univ_hook)
+ evars_typ ctx evars ~hook)
let out_def = function
| Some def -> def
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 361ed1a737..7dcd098183 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -33,7 +33,7 @@ let get_locality id ~kind = function
| Local -> true
| Global -> false
-let declare_definition ident (local, p, k) ?hook ce pl imps =
+let declare_definition ident (local, p, k) ?hook_data ce pl imps =
let fix_exn = Future.fix_exn_of ce.const_entry_body in
let gr = match local with
| Discharge when Lib.sections_are_opened () ->
@@ -49,11 +49,17 @@ let declare_definition ident (local, p, k) ?hook ce pl imps =
in
let () = maybe_declare_manual_implicits false gr imps in
let () = definition_message ident in
- Lemmas.call_hook ~fix_exn ?hook local gr; gr
+ begin
+ match hook_data with
+ | None -> ()
+ | Some (hook, uctx, extra_defs) ->
+ Lemmas.call_hook ~fix_exn ~hook uctx extra_defs local gr
+ end;
+ gr
-let declare_fix ?(opaque = false) (_,poly,_ as kind) pl univs f ((def,_),eff) t imps =
+let declare_fix ?(opaque = false) ?hook_data (_,poly,_ as kind) pl univs f ((def,_),eff) t imps =
let ce = definition_entry ~opaque ~types:t ~univs ~eff def in
- declare_definition f kind ce pl imps
+ declare_definition f kind ?hook_data ce pl imps
let check_definition_evars ~allow_evars sigma =
let env = Global.env () in
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index e455b59ab2..3f95ec7107 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -13,16 +13,26 @@ open Decl_kinds
val get_locality : Id.t -> kind:string -> Decl_kinds.locality -> bool
-val declare_definition : Id.t -> definition_kind ->
- ?hook:Lemmas.declaration_hook ->
- Safe_typing.private_constants Entries.definition_entry -> UnivNames.universe_binders -> Impargs.manual_implicits ->
- GlobRef.t
+val declare_definition
+ : Id.t
+ -> definition_kind
+ -> ?hook_data:(Lemmas.declaration_hook * UState.t * (Id.t * Constr.t) list)
+ -> Safe_typing.private_constants Entries.definition_entry
+ -> UnivNames.universe_binders
+ -> Impargs.manual_implicits
+ -> GlobRef.t
-val declare_fix : ?opaque:bool -> definition_kind ->
- UnivNames.universe_binders -> Entries.universes_entry ->
- Id.t -> Safe_typing.private_constants Entries.proof_output ->
- Constr.types -> Impargs.manual_implicits ->
- GlobRef.t
+val declare_fix
+ : ?opaque:bool
+ -> ?hook_data:(Lemmas.declaration_hook * UState.t * (Id.t * Constr.t) list)
+ -> definition_kind
+ -> UnivNames.universe_binders
+ -> Entries.universes_entry
+ -> Id.t
+ -> Safe_typing.private_constants Entries.proof_output
+ -> Constr.types
+ -> Impargs.manual_implicits
+ -> GlobRef.t
val prepare_definition : allow_evars:bool ->
?opaque:bool -> ?inline:bool -> poly:bool ->
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 83dd1aa8e4..77f125e878 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -34,10 +34,13 @@ open Impargs
module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
-type declaration_hook = Decl_kinds.locality -> GlobRef.t -> unit
+type hook_type = UState.t -> (Id.t * Constr.t) list -> Decl_kinds.locality -> GlobRef.t -> unit
+type declaration_hook = hook_type
+
let mk_hook hook = hook
-let call_hook ?hook ?fix_exn l c =
- try Option.iter (fun hook -> hook l c) hook
+
+let call_hook ?hook ?fix_exn uctx trans l c =
+ try Option.iter (fun hook -> hook uctx trans l c) hook
with e when CErrors.noncritical e ->
let e = CErrors.push e in
let e = Option.cata (fun fix -> fix e) e fix_exn in
@@ -174,7 +177,7 @@ let look_for_possibly_mutual_statements sigma = function
(* Saving a goal *)
-let save ?export_seff id const uctx do_guard (locality,poly,kind) hook =
+let save ?export_seff id const uctx do_guard (locality,poly,kind) hook universes =
let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in
try
let const = adjust_guardness_conditions const do_guard in
@@ -203,7 +206,7 @@ let save ?export_seff id const uctx do_guard (locality,poly,kind) hook =
gr
in
definition_message id;
- call_hook ?hook locality r
+ call_hook ?hook universes [] locality r
with e when CErrors.noncritical e ->
let e = CErrors.push e in
iraise (fix_exn e)
@@ -289,7 +292,7 @@ let warn_let_as_axiom =
(fun id -> strbrk "Let definition" ++ spc () ++ Id.print id ++
spc () ++ strbrk "declared as an axiom.")
-let admit ?hook (id,k,e) pl () =
+let admit ?hook ctx (id,k,e) pl () =
let kn = declare_constant id (ParameterEntry e, IsAssumption Conjectural) in
let () = match k with
| Global, _, _ -> ()
@@ -297,16 +300,15 @@ let admit ?hook (id,k,e) pl () =
in
let () = assumption_message id in
Declare.declare_univ_binders (ConstRef kn) pl;
- call_hook ?hook Global (ConstRef kn)
+ call_hook ?hook ctx [] Global (ConstRef kn)
(* Starting a goal *)
-let universe_proof_terminator ?univ_hook compute_guard =
+let standard_proof_terminator ?(hook : declaration_hook option) compute_guard =
let open Proof_global in
make_terminator begin function
| Admitted (id,k,pe,ctx) ->
- let hook = Option.map (fun univ_hook -> univ_hook (Some ctx)) univ_hook in
- admit ?hook (id,k,pe) (UState.universe_binders ctx) ();
+ let () = admit ?hook ctx (id,k,pe) (UState.universe_binders ctx) () in
Feedback.feedback Feedback.AddedAxiom
| Proved (opaque,idopt, { id; entries=[const]; persistence; universes } ) ->
let is_opaque, export_seff = match opaque with
@@ -317,16 +319,12 @@ let universe_proof_terminator ?univ_hook compute_guard =
let id = match idopt with
| None -> id
| Some { CAst.v = save_id } -> check_anonymity id save_id; save_id in
- let hook = Option.map (fun univ_hook -> univ_hook (Some universes)) univ_hook in
- save ~export_seff id const universes compute_guard persistence hook
+ let () = save ~export_seff id const universes compute_guard persistence hook universes in
+ ()
| Proved (opaque,idopt, _ ) ->
CErrors.anomaly Pp.(str "[universe_proof_terminator] close_proof returned more than one proof term")
end
-let standard_proof_terminator ?hook compute_guard =
- let univ_hook = Option.map (fun hook _ -> hook) hook in
- universe_proof_terminator ?univ_hook compute_guard
-
let initialize_named_context_for_proof () =
let sign = Global.named_context () in
List.fold_right
@@ -335,7 +333,7 @@ let initialize_named_context_for_proof () =
let d = if variable_opacity id then NamedDecl.LocalAssum (id, NamedDecl.get_type d) else d in
Environ.push_named_context_val d signv) sign Environ.empty_named_context_val
-let start_proof id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c =
+let start_proof id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?(hook : declaration_hook option) c =
let terminator = match terminator with
| None -> standard_proof_terminator ?hook compute_guard
| Some terminator -> terminator ?hook compute_guard
@@ -348,20 +346,6 @@ let start_proof id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c
let goals = [ Global.env_of_context sign , c ] in
Proof_global.start_proof sigma id ?pl kind goals terminator
-let start_proof_univs id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?univ_hook c =
- let terminator = match terminator with
- | None ->
- universe_proof_terminator ?univ_hook compute_guard
- | Some terminator -> terminator ?univ_hook compute_guard
- in
- let sign =
- match sign with
- | Some sign -> sign
- | None -> initialize_named_context_for_proof ()
- in
- let goals = [ Global.env_of_context sign , c ] in
- Proof_global.start_proof sigma id ?pl kind goals terminator
-
let rec_tac_initializer finite guard thms snl =
if finite then
match List.map (fun (id,(t,_)) -> (id,t)) thms with
@@ -394,11 +378,7 @@ let start_proof_with_initialization ?hook kind sigma decl recguard thms snl =
match thms with
| [] -> anomaly (Pp.str "No proof to start.")
| (id,(t,(_,imps)))::other_thms ->
- let hook ctx strength ref =
- let ctx = match ctx with
- | None -> UState.empty
- | Some ctx -> ctx
- in
+ let hook ctx _ strength ref =
let other_thms_data =
if List.is_empty other_thms then [] else
(* there are several theorems defined mutually *)
@@ -410,8 +390,8 @@ let start_proof_with_initialization ?hook kind sigma decl recguard thms snl =
let thms_data = (strength,ref,imps)::other_thms_data in
List.iter (fun (strength,ref,imps) ->
maybe_declare_manual_implicits false ref imps;
- call_hook ?hook strength ref) thms_data in
- start_proof_univs id ~pl:decl kind sigma t ~univ_hook:(fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard;
+ call_hook ?hook ctx [] strength ref) thms_data in
+ start_proof id ~pl:decl kind sigma t ~hook ~compute_guard:guard;
ignore (Proof_global.with_current_proof (fun _ p ->
match init_tac with
| None -> p,(true,[])
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index a9a10a6e38..72c666e903 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -13,10 +13,29 @@ open Decl_kinds
type declaration_hook
-val mk_hook : (Decl_kinds.locality -> GlobRef.t -> unit) -> declaration_hook
-val call_hook :
- ?hook:declaration_hook -> ?fix_exn:Future.fix_exn ->
- Decl_kinds.locality -> GlobRef.t -> unit
+(* Hooks allow users of the API to perform arbitrary actions at
+ * proof/definition saving time. For example, to register a constant
+ * as a Coercion, perform some cleanup, update the search database,
+ * etc...
+ *
+ * Here, we use an extended hook type suitable for obligations /
+ * equations.
+ *)
+(** [hook_type] passes to the client:
+ - [ustate]: universe constraints obtained when the term was closed
+ - [(n1,t1),...(nm,tm)]: association list between obligation
+ name and the corresponding defined term (might be a constant,
+ but also an arbitrary term in the Expand case of obligations)
+ - [locality]: Locality of the original declaration
+ - [ref]: identifier of the origianl declaration
+ *)
+type hook_type = UState.t -> (Id.t * Constr.t) list -> Decl_kinds.locality -> GlobRef.t -> unit
+
+val mk_hook : hook_type -> declaration_hook
+val call_hook
+ : ?hook:declaration_hook
+ -> ?fix_exn:Future.fix_exn
+ -> hook_type
val start_proof : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map ->
?terminator:(?hook:declaration_hook -> Proof_global.lemma_possible_guards -> Proof_global.proof_terminator) ->
@@ -24,12 +43,6 @@ val start_proof : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map
?compute_guard:Proof_global.lemma_possible_guards ->
?hook:declaration_hook -> EConstr.types -> unit
-val start_proof_univs : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map ->
- ?terminator:(?univ_hook:(UState.t option -> declaration_hook) -> Proof_global.lemma_possible_guards -> Proof_global.proof_terminator) ->
- ?sign:Environ.named_context_val ->
- ?compute_guard:Proof_global.lemma_possible_guards ->
- ?univ_hook:(UState.t option -> declaration_hook) -> EConstr.types -> unit
-
val start_proof_com :
program_mode:bool -> ?inference_hook:Pretyping.inference_hook ->
?hook:declaration_hook -> goal_kind -> Vernacexpr.proof_expr list ->
@@ -43,11 +56,6 @@ val start_proof_with_initialization :
(EConstr.types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list ->
int list option -> unit
-val universe_proof_terminator :
- ?univ_hook:(UState.t option -> declaration_hook) ->
- Proof_global.lemma_possible_guards ->
- Proof_global.proof_terminator
-
val standard_proof_terminator :
?hook:declaration_hook -> Proof_global.lemma_possible_guards ->
Proof_global.proof_terminator
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index ba78c73131..38cdfc2d7a 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -20,15 +20,6 @@ open Pp
open CErrors
open Util
-type univ_declaration_hook = UState.t -> (Id.t * constr) list -> Decl_kinds.locality -> GlobRef.t -> unit
-let mk_univ_hook f = f
-let call_univ_hook ?univ_hook ?fix_exn uctx trans l c =
- try Option.iter (fun hook -> hook uctx trans l c) univ_hook
- with e when CErrors.noncritical e ->
- let e = CErrors.push e in
- let e = Option.cata (fun fix -> fix e) e fix_exn in
- iraise e
-
module NamedDecl = Context.Named.Declaration
let get_fix_exn, stm_get_fix_exn = Hook.make ()
@@ -321,7 +312,7 @@ type program_info_aux = {
prg_notations : notations ;
prg_kind : definition_kind;
prg_reduce : constr -> constr;
- prg_hook : univ_declaration_hook option;
+ prg_hook : Lemmas.declaration_hook option;
prg_opaque : bool;
prg_sign: named_context_val;
}
@@ -482,9 +473,9 @@ let declare_definition prg =
let ce = definition_entry ~fix_exn ~opaque ~types:typ ~univs body in
let () = progmap_remove prg in
let ubinders = UState.universe_binders uctx in
- let hook = Lemmas.mk_hook (fun l r -> call_univ_hook ?univ_hook:prg.prg_hook ~fix_exn uctx obls l r; ()) in
+ let hook_data = Option.map (fun hook -> hook, uctx, obls) prg.prg_hook in
DeclareDef.declare_definition prg.prg_name
- prg.prg_kind ce ubinders prg.prg_implicits ~hook
+ prg.prg_kind ce ubinders prg.prg_implicits ?hook_data
let rec lam_index n t acc =
match Constr.kind t with
@@ -559,14 +550,16 @@ let declare_mutual_definition l =
(* Declare the recursive definitions *)
let univs = UState.univ_entry ~poly first.prg_ctx in
let fix_exn = Hook.get get_fix_exn () in
- let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) UnivNames.empty_binders univs)
- fixnames fixdecls fixtypes fiximps in
- (* Declare notations *)
- List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations;
- Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
- let gr = List.hd kns in
- call_univ_hook ?univ_hook:first.prg_hook ~fix_exn first.prg_ctx obls local gr;
- List.iter progmap_remove l; gr
+ let kns = List.map4
+ (DeclareDef.declare_fix ~opaque (local, poly, kind) UnivNames.empty_binders univs)
+ fixnames fixdecls fixtypes fiximps
+ in
+ (* Declare notations *)
+ List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations;
+ Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
+ let gr = List.hd kns in
+ Lemmas.call_hook ?hook:first.prg_hook ~fix_exn first.prg_ctx obls local gr;
+ List.iter progmap_remove l; gr
let decompose_lam_prod c ty =
let open Context.Rel.Declaration in
@@ -663,7 +656,7 @@ let declare_obligation prg obl body ty uctx =
in
true, { obl with obl_body = body }
-let init_prog_info ?(opaque = false) ?univ_hook sign n udecl b t ctx deps fixkind
+let init_prog_info ?(opaque = false) ?hook sign n udecl b t ctx deps fixkind
notations obls impls kind reduce =
let obls', b =
match b with
@@ -689,7 +682,7 @@ let init_prog_info ?(opaque = false) ?univ_hook sign n udecl b t ctx deps fixkin
prg_obligations = (obls', Array.length obls');
prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ;
prg_implicits = impls; prg_kind = kind; prg_reduce = reduce;
- prg_hook = univ_hook; prg_opaque = opaque;
+ prg_hook = hook; prg_opaque = opaque;
prg_sign = sign }
let map_cardinal m =
@@ -844,9 +837,9 @@ let solve_by_tac ?loc name evi t poly ctx =
warn_solve_errored ?loc err;
None
-let obligation_terminator ?univ_hook name num guard auto pf =
+let obligation_terminator ?hook name num guard auto pf =
let open Proof_global in
- let term = Lemmas.universe_proof_terminator ?univ_hook guard in
+ let term = Lemmas.standard_proof_terminator ?hook guard in
match pf with
| Admitted _ -> apply_terminator term pf
| Proved (opq, id, { entries=[entry]; universes=uctx } ) -> begin
@@ -912,7 +905,7 @@ let obligation_terminator ?univ_hook name num guard auto pf =
| Proved (_, _, _ ) ->
CErrors.anomaly Pp.(str "[obligation_terminator] close_proof returned more than one proof term")
-let obligation_hook prg obl num auto ctx' _ gr =
+let obligation_hook prg obl num auto ctx' _ _ gr =
let obls, rem = prg.prg_obligations in
let cst = match gr with GlobRef.ConstRef cst -> cst | _ -> assert false in
let transparent = evaluable_constant cst (Global.env ()) in
@@ -922,7 +915,6 @@ let obligation_hook prg obl num auto ctx' _ gr =
if not transparent then err_not_transp ()
| _ -> ()
in
- let ctx' = match ctx' with None -> prg.prg_ctx | Some ctx' -> ctx' in
let inst, ctx' =
if not (pi2 prg.prg_kind) (* Not polymorphic *) then
(* The universe context was declared globally, we continue
@@ -969,11 +961,11 @@ let rec solve_obligation prg num tac =
let evd = Evd.from_ctx prg.prg_ctx in
let evd = Evd.update_sigma_env evd (Global.env ()) in
let auto n tac oblset = auto_solve_obligations n ~oblset tac in
- let terminator ?univ_hook guard =
+ let terminator ?hook guard =
Proof_global.make_terminator
- (obligation_terminator ?univ_hook prg.prg_name num guard auto) in
- let univ_hook ctx = Lemmas.mk_hook (obligation_hook prg obl num auto ctx) in
- let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator ~univ_hook in
+ (obligation_terminator ?hook prg.prg_name num guard auto) in
+ let hook = Lemmas.mk_hook (obligation_hook prg obl num auto) in
+ let () = Lemmas.start_proof ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator ~hook in
let _ = Pfedit.by !default_tactic in
Option.iter (fun tac -> Proof_global.set_endline_tactic tac) tac
@@ -1110,10 +1102,10 @@ let show_term n =
let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl)
?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
- ?(reduce=reduce) ?univ_hook ?(opaque = false) obls =
+ ?(reduce=reduce) ?hook ?(opaque = false) obls =
let sign = Lemmas.initialize_named_context_for_proof () in
let info = Id.print n ++ str " has type-checked" in
- let prg = init_prog_info sign ~opaque n univdecl term t ctx [] None [] obls implicits kind reduce ?univ_hook in
+ let prg = init_prog_info sign ~opaque n univdecl term t ctx [] None [] obls implicits kind reduce ?hook in
let obls,_ = prg.prg_obligations in
if Int.equal (Array.length obls) 0 then (
Flags.if_verbose Feedback.msg_info (info ++ str ".");
@@ -1130,13 +1122,13 @@ let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl)
let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic
?(kind=Global,false,Definition) ?(reduce=reduce)
- ?univ_hook ?(opaque = false) notations fixkind =
+ ?hook ?(opaque = false) notations fixkind =
let sign = Lemmas.initialize_named_context_for_proof () in
let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
List.iter
(fun (n, b, t, imps, obls) ->
let prg = init_prog_info sign ~opaque n univdecl (Some b) t ctx deps (Some fixkind)
- notations obls imps kind reduce ?univ_hook
+ notations obls imps kind reduce ?hook
in progmap_add n (CEphemeron.create prg)) l;
let _defined =
List.fold_left (fun finished x ->
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 4eef668f56..c5720363b4 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -13,12 +13,6 @@ open Constr
open Evd
open Names
-type univ_declaration_hook
-val mk_univ_hook : (UState.t -> (Id.t * constr) list -> Decl_kinds.locality -> GlobRef.t -> unit) ->
- univ_declaration_hook
-val call_univ_hook : ?univ_hook:univ_declaration_hook -> ?fix_exn:Future.fix_exn ->
- UState.t -> (Id.t * constr) list -> Decl_kinds.locality -> GlobRef.t -> unit
-
(* This is a hack to make it possible for Obligations to craft a Qed
* behind the scenes. The fix_exn the Stm attaches to the Future proof
* is not available here, so we provide a side channel to get it *)
@@ -58,14 +52,19 @@ type progress = (* Resolution status of a program *)
val default_tactic : unit Proofview.tactic ref
-val add_definition : Names.Id.t -> ?term:constr -> types ->
- UState.t ->
- ?univdecl:UState.universe_decl -> (* Universe binders and constraints *)
- ?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list ->
- ?kind:Decl_kinds.definition_kind ->
- ?tactic:unit Proofview.tactic ->
- ?reduce:(constr -> constr) ->
- ?univ_hook:univ_declaration_hook -> ?opaque:bool -> obligation_info -> progress
+val add_definition
+ : Names.Id.t
+ -> ?term:constr -> types
+ -> UState.t
+ -> ?univdecl:UState.universe_decl (* Universe binders and constraints *)
+ -> ?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list
+ -> ?kind:Decl_kinds.definition_kind
+ -> ?tactic:unit Proofview.tactic
+ -> ?reduce:(constr -> constr)
+ -> ?hook:Lemmas.declaration_hook
+ -> ?opaque:bool
+ -> obligation_info
+ -> progress
type notations =
(lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
@@ -82,7 +81,7 @@ val add_mutual_definitions :
?tactic:unit Proofview.tactic ->
?kind:Decl_kinds.definition_kind ->
?reduce:(constr -> constr) ->
- ?univ_hook:univ_declaration_hook -> ?opaque:bool ->
+ ?hook:Lemmas.declaration_hook -> ?opaque:bool ->
notations ->
fixpoint_kind -> unit
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index d511bcd4fd..11b64a5247 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -542,7 +542,7 @@ let vernac_definition_hook p = function
| Coercion ->
Some (Class.add_coercion_hook p)
| CanonicalStructure ->
- Some (Lemmas.mk_hook (fun _ -> Recordops.declare_canonical_structure))
+ Some (Lemmas.mk_hook (fun _ _ _ -> Recordops.declare_canonical_structure))
| SubClass ->
Some (Class.add_subclass_hook p)
| _ -> None
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:41:04 +0000