aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/ci/user-overlays/08704-ejgallego-vernac+monify_hook.sh15
-rw-r--r--plugins/funind/indfun_common.mli2
-rw-r--r--vernac/class.mli4
-rw-r--r--vernac/classes.ml6
-rw-r--r--vernac/comDefinition.ml6
-rw-r--r--vernac/comDefinition.mli2
-rw-r--r--vernac/comProgramFixpoint.ml6
-rw-r--r--vernac/declareDef.ml4
-rw-r--r--vernac/declareDef.mli2
-rw-r--r--vernac/lemmas.ml2
-rw-r--r--vernac/lemmas.mli29
-rw-r--r--vernac/obligations.ml18
-rw-r--r--vernac/obligations.mli8
-rw-r--r--vernac/vernacentries.ml8
14 files changed, 68 insertions, 44 deletions
diff --git a/dev/ci/user-overlays/08704-ejgallego-vernac+monify_hook.sh b/dev/ci/user-overlays/08704-ejgallego-vernac+monify_hook.sh
new file mode 100644
index 0000000000..b3a9f67e00
--- /dev/null
+++ b/dev/ci/user-overlays/08704-ejgallego-vernac+monify_hook.sh
@@ -0,0 +1,15 @@
+if [ "$CI_PULL_REQUEST" = "8704" ] || [ "$CI_BRANCH" = "vernac+monify_hook" ]; then
+
+ # ltac2_CI_REF=rm-section-path
+ # ltac2_CI_GITURL=https://github.com/maximedenes/ltac2
+
+ plugin_tutorial_CI_REF=vernac+monify_hook
+ plugin_tutorial_CI_GITURL=https://github.com/ejgallego/plugin_tutorials
+
+ Elpi_CI_REF=vernac+monify_hook
+ Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
+
+ Equations_CI_REF=vernac+monify_hook
+ Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+fi
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 7e52ee224f..1b4c1248a5 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -46,7 +46,7 @@ val jmeq : unit -> EConstr.constr
val jmeq_refl : unit -> EConstr.constr
val save : bool -> Id.t -> Safe_typing.private_constants Entries.definition_entry -> Decl_kinds.goal_kind ->
- unit Lemmas.declaration_hook CEphemeron.key -> unit
+ Lemmas.declaration_hook CEphemeron.key -> unit
(* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and
abort the proof
diff --git a/vernac/class.mli b/vernac/class.mli
index f7e837f3bb..80d6d4383c 100644
--- a/vernac/class.mli
+++ b/vernac/class.mli
@@ -42,8 +42,8 @@ val try_add_new_coercion_with_source : GlobRef.t -> local:bool ->
val try_add_new_identity_coercion : Id.t -> local:bool ->
Decl_kinds.polymorphic -> source:cl_typ -> target:cl_typ -> unit
-val add_coercion_hook : Decl_kinds.polymorphic -> unit Lemmas.declaration_hook
+val add_coercion_hook : Decl_kinds.polymorphic -> Lemmas.declaration_hook
-val add_subclass_hook : Decl_kinds.polymorphic -> unit Lemmas.declaration_hook
+val add_subclass_hook : Decl_kinds.polymorphic -> Lemmas.declaration_hook
val class_of_global : GlobRef.t -> cl_typ
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 37ee33b19f..09e2b8df45 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -149,7 +149,7 @@ let do_abstract_instance env sigma ?hook ~global ~poly k u ctx ctx' pri decl imp
let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl len term termtype =
let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in
if program_mode then
- let hook vis gr _ =
+ let hook _ vis gr =
let cst = match gr with ConstRef kn -> kn | _ -> assert false in
Impargs.declare_manual_implicits false gr ~enriching:false [imps];
let pri = intern_info pri in
@@ -163,7 +163,7 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id
in obls, Some constr, typ
| None -> [||], None, termtype
in
- let hook = Lemmas.mk_hook hook in
+ let hook = Obligations.mk_univ_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) ~hook obls)
@@ -425,7 +425,7 @@ let context poly l =
| Some b ->
let decl = (Discharge, poly, Definition) in
let entry = Declare.definition_entry ~univs ~types:t b in
- let hook = Lemmas.mk_hook (fun _ gr -> gr) in
+ let hook = Lemmas.mk_hook (fun _ _ -> ()) in
let _ = DeclareDef.declare_definition id decl entry UnivNames.empty_binders [] hook in
Lib.sections_are_opened () || Lib.is_modtype_strict ()
in
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index a8d7946429..5d17662d1a 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -127,10 +127,8 @@ let do_definition ~program_mode ident k univdecl bl red_option c ctypopt hook =
Obligations.eterm_obligations env ident evd 0 c typ
in
let ctx = Evd.evar_universe_context evd in
- let hook = Lemmas.mk_hook (fun l r _ -> Lemmas.call_hook (fun exn -> exn) hook l r) in
+ let hook = Obligations.mk_univ_hook (fun _ l r -> Lemmas.call_hook (fun x -> x) hook l r) in
ignore(Obligations.add_definition
ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ~hook obls)
else let ce = check_definition def in
- ignore(DeclareDef.declare_definition ident k ce (Evd.universe_binders evd) imps
- (Lemmas.mk_hook
- (fun l r -> Lemmas.call_hook (fun exn -> exn) hook l r;r)))
+ ignore(DeclareDef.declare_definition ident k ce (Evd.universe_binders evd) imps hook)
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index 7f1c902c0f..58007e6a88 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -19,7 +19,7 @@ open Constrexpr
val do_definition : program_mode:bool ->
Id.t -> definition_kind -> universe_decl_expr option ->
local_binder_expr list -> red_expr option -> constr_expr ->
- constr_expr option -> unit Lemmas.declaration_hook -> unit
+ constr_expr option -> Lemmas.declaration_hook -> unit
(************************************************************************)
(** Internal API *)
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index c33e6b72c6..ab898644c0 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -192,7 +192,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
let name = add_suffix recname "_func" in
(* XXX: Mutating the evar_map in the hook! *)
(* XXX: Likely the sigma is out of date when the hook is called .... *)
- let hook sigma l gr _ =
+ let hook sigma _ l gr =
let sigma, h_body = Evarutil.new_global sigma gr in
let body = it_mkLambda_or_LetIn (mkApp (h_body, [|make|])) binders_rel in
let ty = it_mkProd_or_LetIn top_arity binders_rel in
@@ -211,13 +211,13 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
hook, name, typ
else
let typ = it_mkProd_or_LetIn top_arity binders_rel in
- let hook sigma l gr _ =
+ let hook sigma _ l gr =
if Impargs.is_implicit_args () || not (List.is_empty impls) then
Impargs.declare_manual_implicits false gr [impls]
in hook, recname, typ
in
(* XXX: Capturing sigma here... bad bad *)
- let hook = Lemmas.mk_hook (hook sigma) in
+ let hook = Obligations.mk_univ_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
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 77177dfa41..7426c128cc 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -58,9 +58,9 @@ let declare_definition ident (local, p, k) ce pl imps hook =
gr
| Discharge | Local | Global ->
declare_global_definition ident ce local k pl imps in
- Lemmas.call_hook fix_exn hook local r
+ Lemmas.call_hook fix_exn hook local r; r
let declare_fix ?(opaque = false) (_,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 (Lemmas.mk_hook (fun _ r -> r))
+ declare_definition f kind ce pl imps (Lemmas.mk_hook (fun _ _ -> ()))
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index c5e704a5e9..da11d4d9c0 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -15,7 +15,7 @@ val get_locality : Id.t -> kind:string -> Decl_kinds.locality -> bool
val declare_definition : Id.t -> definition_kind ->
Safe_typing.private_constants Entries.definition_entry -> UnivNames.universe_binders -> Impargs.manual_implicits ->
- GlobRef.t Lemmas.declaration_hook -> GlobRef.t
+ Lemmas.declaration_hook -> GlobRef.t
val declare_fix : ?opaque:bool -> definition_kind ->
UnivNames.universe_binders -> Entries.constant_universes_entry ->
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index bbefd2dfe7..a99aace399 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -34,7 +34,7 @@ open Impargs
module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
-type 'a declaration_hook = Decl_kinds.locality -> GlobRef.t -> 'a
+type declaration_hook = Decl_kinds.locality -> GlobRef.t -> unit
let mk_hook hook = hook
let call_hook fix_exn hook l c =
try hook l c
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index d8e337c09c..195fcbf4ca 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -11,44 +11,41 @@
open Names
open Decl_kinds
-type 'a declaration_hook
-val mk_hook :
- (Decl_kinds.locality -> GlobRef.t -> 'a) -> 'a declaration_hook
-
-val call_hook :
- Future.fix_exn -> 'a declaration_hook -> Decl_kinds.locality -> GlobRef.t -> 'a
+type declaration_hook
+val mk_hook : (Decl_kinds.locality -> GlobRef.t -> unit) -> declaration_hook
+val call_hook : Future.fix_exn -> declaration_hook -> Decl_kinds.locality -> GlobRef.t -> unit
val start_proof : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map ->
- ?terminator:(Proof_global.lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) ->
+ ?terminator:(Proof_global.lemma_possible_guards -> declaration_hook -> Proof_global.proof_terminator) ->
?sign:Environ.named_context_val -> EConstr.types ->
- ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards ->
- unit declaration_hook -> unit
+ ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards ->
+ declaration_hook -> unit
val start_proof_univs : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map ->
- ?terminator:(Proof_global.lemma_possible_guards -> (UState.t option -> unit declaration_hook) -> Proof_global.proof_terminator) ->
+ ?terminator:(Proof_global.lemma_possible_guards -> (UState.t option -> declaration_hook) -> Proof_global.proof_terminator) ->
?sign:Environ.named_context_val -> EConstr.types ->
- ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards ->
- (UState.t option -> unit declaration_hook) -> unit
+ ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards ->
+ (UState.t option -> declaration_hook) -> unit
val start_proof_com :
?inference_hook:Pretyping.inference_hook ->
goal_kind -> Vernacexpr.proof_expr list ->
- unit declaration_hook -> unit
+ declaration_hook -> unit
val start_proof_with_initialization :
goal_kind -> Evd.evar_map -> UState.universe_decl ->
(bool * Proof_global.lemma_possible_guards * unit Proofview.tactic list option) option ->
(Id.t (* name of thm *) *
(EConstr.types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list
- -> int list option -> unit declaration_hook -> unit
+ -> int list option -> declaration_hook -> unit
val universe_proof_terminator :
Proof_global.lemma_possible_guards ->
- (UState.t option -> unit declaration_hook) ->
+ (UState.t option -> declaration_hook) ->
Proof_global.proof_terminator
val standard_proof_terminator :
- Proof_global.lemma_possible_guards -> unit declaration_hook ->
+ Proof_global.lemma_possible_guards -> declaration_hook ->
Proof_global.proof_terminator
val fresh_name_for_anonymous_theorem : unit -> Id.t
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 757a56d436..bdf74bf63d 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -20,6 +20,14 @@ open Pp
open CErrors
open Util
+type univ_declaration_hook = UState.t -> Decl_kinds.locality -> GlobRef.t -> unit
+let mk_univ_hook f = f
+let call_univ_hook fix_exn hook uctx l c =
+ try hook uctx l c
+ with e when CErrors.noncritical e ->
+ let e = CErrors.push e in
+ iraise (fix_exn e)
+
module NamedDecl = Context.Named.Declaration
let get_fix_exn, stm_get_fix_exn = Hook.make ()
@@ -314,7 +322,7 @@ type program_info_aux = {
prg_notations : notations ;
prg_kind : definition_kind;
prg_reduce : constr -> constr;
- prg_hook : (UState.t -> unit) Lemmas.declaration_hook;
+ prg_hook : univ_declaration_hook;
prg_opaque : bool;
prg_sign: named_context_val;
}
@@ -488,7 +496,7 @@ let declare_definition prg =
let ubinders = UState.universe_binders uctx in
DeclareDef.declare_definition prg.prg_name
prg.prg_kind ce ubinders prg.prg_implicits
- (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r uctx; r))
+ (Lemmas.mk_hook (fun l r -> call_univ_hook fix_exn prg.prg_hook uctx l r ; ()))
let rec lam_index n t acc =
match Constr.kind t with
@@ -562,7 +570,7 @@ let declare_mutual_definition l =
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 fix_exn first.prg_hook local gr first.prg_ctx;
+ call_univ_hook fix_exn first.prg_hook first.prg_ctx local gr;
List.iter progmap_remove l; gr
let decompose_lam_prod c ty =
@@ -1099,7 +1107,7 @@ let show_term n =
let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl)
?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
- ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) obls =
+ ?(reduce=reduce) ?(hook=mk_univ_hook (fun _ _ _ -> ())) ?(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 hook in
@@ -1119,7 +1127,7 @@ 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)
- ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) notations fixkind =
+ ?(hook=mk_univ_hook (fun _ _ _ -> ())) ?(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
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index a37c30aafc..80294c7a76 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -13,6 +13,10 @@ open Constr
open Evd
open Names
+type univ_declaration_hook
+val mk_univ_hook : (UState.t -> Decl_kinds.locality -> GlobRef.t -> unit) -> univ_declaration_hook
+val call_univ_hook : Future.fix_exn -> univ_declaration_hook -> UState.t -> 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 *)
@@ -59,7 +63,7 @@ val add_definition : Names.Id.t -> ?term:constr -> types ->
?kind:Decl_kinds.definition_kind ->
?tactic:unit Proofview.tactic ->
?reduce:(constr -> constr) ->
- ?hook:(UState.t -> unit) Lemmas.declaration_hook -> ?opaque:bool -> obligation_info -> progress
+ ?hook:univ_declaration_hook -> ?opaque:bool -> obligation_info -> progress
type notations =
(lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
@@ -76,7 +80,7 @@ val add_mutual_definitions :
?tactic:unit Proofview.tactic ->
?kind:Decl_kinds.definition_kind ->
?reduce:(constr -> constr) ->
- ?hook:(UState.t -> unit) Lemmas.declaration_hook -> ?opaque:bool ->
+ ?hook:univ_declaration_hook -> ?opaque:bool ->
notations ->
fixpoint_kind -> unit
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 24f6ba3049..32c61378db 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -479,10 +479,12 @@ let start_proof_and_print k l hook =
let no_hook = Lemmas.mk_hook (fun _ _ -> ())
let vernac_definition_hook p = function
-| Coercion -> Class.add_coercion_hook p
+| Coercion ->
+ Class.add_coercion_hook p
| CanonicalStructure ->
- Lemmas.mk_hook (fun _ -> Recordops.declare_canonical_structure)
-| SubClass -> Class.add_subclass_hook p
+ Lemmas.mk_hook (fun _ -> Recordops.declare_canonical_structure)
+| SubClass ->
+ Class.add_subclass_hook p
| _ -> no_hook
let vernac_definition ~atts discharge kind ({loc;v=id}, pl) def =
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:02:27 +0000