aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/derive/derive.ml4
-rw-r--r--stm/stm.ml11
-rw-r--r--vernac/lemmas.ml70
-rw-r--r--vernac/lemmas.mli27
-rw-r--r--vernac/obligations.ml12
-rw-r--r--vernac/vernacentries.mli2
-rw-r--r--vernac/vernacstate.ml6
-rw-r--r--vernac/vernacstate.mli2
8 files changed, 77 insertions, 57 deletions
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index aad3967f6d..f8b5f455d1 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -56,9 +56,9 @@ let start_deriving f suchthat name : Lemmas.t =
let (opaque,f_def,lemma_def) =
match com with
| Lemmas.Admitted _ -> CErrors.user_err Pp.(str "Admitted isn't supported in Derive.")
- | Lemmas.Proved (_,Some _,_) ->
+ | Lemmas.Proved (_,Some _,_, _) ->
CErrors.user_err Pp.(str "Cannot save a proof of Derive with an explicit name.")
- | Lemmas.Proved (opaque, None, obj) ->
+ | Lemmas.Proved (opaque, None, obj,_) ->
match Proof_global.(obj.entries) with
| [_;f_def;lemma_def] ->
opaque <> Proof_global.Transparent , f_def , lemma_def
diff --git a/stm/stm.ml b/stm/stm.ml
index d77e37c910..a0247e0d8f 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1532,14 +1532,15 @@ end = struct (* {{{ *)
(* Unfortunately close_future_proof and friends are not pure so we need
to set the state manually here *)
State.unfreeze st;
- let pobject, _ =
+ let pobject, _terminator, _hook =
PG_compat.close_future_proof ~opaque ~feedback_id:stop (Future.from_val ~fix_exn p) in
+
let terminator = (* The one sent by master is an InvalidKey *)
Lemmas.(standard_proof_terminator []) in
let st = Vernacstate.freeze_interp_state ~marshallable:false in
stm_vernac_interp stop
- ~proof:(pobject, terminator) st
+ ~proof:(pobject, terminator, None) st
{ verbose = false; indentation = 0; strlen = 0;
expr = CAst.make ?loc @@ VernacExpr ([], VernacEndProof (Proved (opaque,None))) }) in
ignore(Future.join checked_proof);
@@ -1676,10 +1677,10 @@ end = struct (* {{{ *)
let opaque = Proof_global.Opaque in
(* The original terminator, a hook, has not been saved in the .vio*)
- let pterm, _invalid_terminator =
+ let pterm, _invalid_terminator, _hook =
PG_compat.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in
- let proof = pterm , Lemmas.standard_proof_terminator [] in
+ let proof = pterm , Lemmas.standard_proof_terminator [], None in
(* We jump at the beginning since the kernel handles side effects by also
* looking at the ones that happen to be present in the current env *)
@@ -1734,7 +1735,7 @@ end = struct (* {{{ *)
| `ERROR -> exit 1
| `ERROR_ADMITTED -> cst, false
| `OK_ADMITTED -> cst, false
- | `OK (po,_) ->
+ | `OK (po,_,_) ->
let con =
Nametab.locate_constant
(Libnames.qualid_of_ident po.Proof_global.id) in
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 7aba64fb93..695da1fcee 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -34,12 +34,12 @@ module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
type hook_type = UState.t -> (Id.t * Constr.t) list -> Decl_kinds.locality -> GlobRef.t -> unit
-type declaration_hook = hook_type
+type declaration_hook = hook_type CEphemeron.key
-let mk_hook hook = hook
+let mk_hook hook = CEphemeron.create hook
let call_hook ?hook ?fix_exn uctx trans l c =
- try Option.iter (fun hook -> hook uctx trans l c) hook
+ try Option.iter (fun hook -> CEphemeron.get 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
@@ -49,10 +49,18 @@ let call_hook ?hook ?fix_exn uctx trans l c =
[that can be saved] *)
type proof_ending =
- | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t
- | Proved of Proof_global.opacity_flag *
- lident option *
- Proof_global.proof_object
+ | Admitted of
+ Names.Id.t *
+ Decl_kinds.goal_kind *
+ Entries.parameter_entry *
+ UState.t *
+ declaration_hook option
+
+ | Proved of
+ Proof_global.opacity_flag *
+ lident option *
+ Proof_global.proof_object *
+ declaration_hook option
type proof_terminator = (proof_ending -> unit) CEphemeron.key
@@ -60,9 +68,10 @@ type proof_terminator = (proof_ending -> unit) CEphemeron.key
type t =
{ proof : Proof_global.t
; terminator : proof_terminator
+ ; hook : declaration_hook option
}
-let pf_map f { proof; terminator} = { proof = f proof; terminator }
+let pf_map f { proof; terminator; hook } = { proof = f proof; terminator; hook }
let pf_fold f ps = f ps.proof
let set_endline_tactic t = pf_map (Proof_global.set_endline_tactic t)
@@ -76,12 +85,13 @@ let apply_terminator f = CEphemeron.get f
(** Gets the current terminator without checking that the proof has
been completed. Useful for the likes of [Admitted]. *)
let get_terminator ps = ps.terminator
+let get_hook ps = ps.hook
end
-let by tac { proof; terminator } =
+let by tac { proof; terminator; hook } =
let proof, res = Pfedit.by tac proof in
- { proof; terminator}, res
+ { proof; terminator; hook}, res
(* Support for mutually proved theorems *)
@@ -316,13 +326,13 @@ let admit ?hook ctx (id,k,e) pl () =
(* Starting a goal *)
-let standard_proof_terminator ?(hook : declaration_hook option) compute_guard =
+let standard_proof_terminator compute_guard =
let open Proof_global in
- CEphemeron.create begin function
- | Admitted (id,k,pe,ctx) ->
+ Internal.make_terminator begin function
+ | Admitted (id,k,pe,ctx,hook) ->
let () = admit ?hook ctx (id,k,pe) (UState.universe_binders ctx) () in
Feedback.feedback Feedback.AddedAxiom
- | Proved (opaque,idopt, { id; entries=[const]; persistence; universes } ) ->
+ | Proved (opaque,idopt, { id; entries=[const]; persistence; universes }, hook ) ->
let is_opaque, export_seff = match opaque with
| Transparent -> false, true
| Opaque -> true, false
@@ -333,7 +343,7 @@ let standard_proof_terminator ?(hook : declaration_hook option) compute_guard =
| Some { CAst.v = save_id } -> check_anonymity id save_id; save_id in
let () = save ~export_seff id const universes compute_guard persistence hook universes in
()
- | Proved (opaque,idopt, _ ) ->
+ | Proved (opaque,idopt, _, hook) ->
CErrors.anomaly Pp.(str "[universe_proof_terminator] close_proof returned more than one proof term")
end
@@ -381,8 +391,8 @@ end
let start_lemma id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c =
let terminator = match terminator with
- | None -> standard_proof_terminator ?hook compute_guard
- | Some terminator -> terminator ?hook compute_guard
+ | None -> standard_proof_terminator compute_guard
+ | Some terminator -> terminator compute_guard
in
let sign =
match sign with
@@ -391,15 +401,15 @@ let start_lemma id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c
in
let goals = [ Global.env_of_context sign , c ] in
let proof = Proof_global.start_proof sigma id ?pl kind goals in
- { proof ; terminator }
+ { proof ; terminator; hook }
let start_dependent_lemma id ?pl kind ?terminator ?sign ?(compute_guard=[]) ?hook telescope =
let terminator = match terminator with
- | None -> standard_proof_terminator ?hook compute_guard
- | Some terminator -> terminator ?hook compute_guard
+ | None -> standard_proof_terminator compute_guard
+ | Some terminator -> terminator compute_guard
in
let proof = Proof_global.start_dependent_proof id ?pl kind telescope in
- { proof ; terminator }
+ { proof ; terminator; hook }
let rec_tac_initializer finite guard thms snl =
if finite then
@@ -447,6 +457,7 @@ let start_lemma_with_initialization ?hook kind sigma decl recguard thms snl =
List.iter (fun (ref,imps) ->
maybe_declare_manual_implicits false ref imps;
call_hook ?hook ctx [] strength ref) thms_data in
+ let hook = mk_hook hook in
let lemma = start_lemma id ~pl:decl kind sigma t ~hook ~compute_guard:guard in
let lemma = pf_map (Proof_global.map_proof (fun p ->
match init_tac with
@@ -505,7 +516,7 @@ let save_lemma_admitted ?proof ~(lemma : t) =
let pe =
let open Proof_global in
match proof with
- | Some ({ id; entries; persistence = k; universes }, _) ->
+ | Some ({ id; entries; persistence = k; universes }, _, hook) ->
if List.length entries <> 1 then
user_err Pp.(str "Admitted does not support multiple statements");
let { const_entry_secctx; const_entry_type } = List.hd entries in
@@ -514,7 +525,7 @@ let save_lemma_admitted ?proof ~(lemma : t) =
let typ = Option.get const_entry_type in
let ctx = UState.univ_entry ~poly:(pi2 k) universes in
let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in
- Admitted(id, k, (sec_vars, (typ, ctx), None), universes)
+ Admitted(id, k, (sec_vars, (typ, ctx), None), universes, hook)
| None ->
let pftree = Proof_global.get_proof lemma.proof in
let gk = Proof_global.get_persistence lemma.proof in
@@ -542,7 +553,7 @@ let save_lemma_admitted ?proof ~(lemma : t) =
| _ -> None in
let decl = Proof_global.get_universe_decl lemma.proof in
let ctx = UState.check_univ_decl ~poly universes decl in
- Admitted(name,gk,(sec_vars, (typ, ctx), None), universes)
+ Admitted(name,gk,(sec_vars, (typ, ctx), None), universes, lemma.hook)
in
CEphemeron.get lemma.terminator pe
@@ -550,13 +561,14 @@ let save_lemma_proved ?proof ?lemma ~opaque ~idopt =
(* Invariant (uh) *)
if Option.is_empty lemma && Option.is_empty proof then
user_err (str "No focused proof (No proof-editing in progress).");
- let (proof_obj,terminator) =
+ let proof_obj,terminator, hook =
match proof with
| None ->
(* XXX: The close_proof and proof state API should be refactored
so it is possible to insert proofs properly into the state *)
- let { proof; terminator } = Option.get lemma in
- Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) proof, terminator
- | Some proof -> proof
+ let { proof; terminator; hook } = Option.get lemma in
+ Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) proof, terminator, hook
+ | Some (proof, terminator, hook) ->
+ proof, terminator, hook
in
- CEphemeron.get terminator (Proved (opaque,idopt,proof_obj))
+ CEphemeron.get terminator (Proved (opaque,idopt,proof_obj,hook))
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 25c5b24e91..03cd45b8bf 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -65,8 +65,7 @@ module Stack : sig
end
val standard_proof_terminator
- : ?hook:declaration_hook
- -> Proof_global.lemma_possible_guards
+ : Proof_global.lemma_possible_guards
-> proof_terminator
val set_endline_tactic : Genarg.glob_generic_argument -> t -> t
@@ -82,7 +81,7 @@ val start_lemma
-> ?pl:UState.universe_decl
-> goal_kind
-> Evd.evar_map
- -> ?terminator:(?hook:declaration_hook -> Proof_global.lemma_possible_guards -> proof_terminator)
+ -> ?terminator:(Proof_global.lemma_possible_guards -> proof_terminator)
-> ?sign:Environ.named_context_val
-> ?compute_guard:Proof_global.lemma_possible_guards
-> ?hook:declaration_hook
@@ -93,7 +92,7 @@ val start_dependent_lemma
: Id.t
-> ?pl:UState.universe_decl
-> goal_kind
- -> ?terminator:(?hook:declaration_hook -> Proof_global.lemma_possible_guards -> proof_terminator)
+ -> ?terminator:(Proof_global.lemma_possible_guards -> proof_terminator)
-> ?sign:Environ.named_context_val
-> ?compute_guard:Proof_global.lemma_possible_guards
-> ?hook:declaration_hook
@@ -126,12 +125,12 @@ val initialize_named_context_for_proof : unit -> Environ.named_context_val
(** {6 Saving proofs } *)
val save_lemma_admitted
- : ?proof:(Proof_global.proof_object * proof_terminator)
+ : ?proof:(Proof_global.proof_object * proof_terminator * declaration_hook option)
-> lemma:t
-> unit
val save_lemma_proved
- : ?proof:(Proof_global.proof_object * proof_terminator)
+ : ?proof:(Proof_global.proof_object * proof_terminator * declaration_hook option)
-> ?lemma:t
-> opaque:Proof_global.opacity_flag
-> idopt:Names.lident option
@@ -139,16 +138,24 @@ val save_lemma_proved
(* API to build a terminator, should go away *)
type proof_ending =
- | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t
- | Proved of Proof_global.opacity_flag *
- Names.lident option *
- Proof_global.proof_object
+ | Admitted of
+ Names.Id.t *
+ Decl_kinds.goal_kind *
+ Entries.parameter_entry *
+ UState.t *
+ declaration_hook option
+ | Proved of
+ Proof_global.opacity_flag *
+ lident option *
+ Proof_global.proof_object *
+ declaration_hook option
(** This stuff is internal and will be removed in the future. *)
module Internal : sig
(** Only needed due to the Proof_global compatibility layer. *)
val get_terminator : t -> proof_terminator
+ val get_hook : t -> declaration_hook option
(** Only needed by obligations, should be reified soon *)
val make_terminator : (proof_ending -> unit) -> proof_terminator
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 6ef2f80067..4a564e705e 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -839,13 +839,13 @@ let solve_by_tac ?loc name evi t poly ctx =
warn_solve_errored ?loc err;
None
-let obligation_terminator ?hook name num guard auto pf =
+let obligation_terminator name num guard auto pf =
let open Proof_global in
let open Lemmas in
- let term = standard_proof_terminator ?hook guard in
+ let term = standard_proof_terminator guard in
match pf with
| Admitted _ -> Internal.apply_terminator term pf
- | Proved (opq, id, { entries=[entry]; universes=uctx } ) -> begin
+ | Proved (opq, id, { entries=[entry]; universes=uctx }, hook ) -> begin
let env = Global.env () in
let ty = entry.Entries.const_entry_type in
let body, eff = Future.force entry.const_entry_body in
@@ -905,7 +905,7 @@ let obligation_terminator ?hook name num guard auto pf =
let e = CErrors.push e in
pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e))
end
- | Proved (_, _, _ ) ->
+ | Proved (_, _, _,_ ) ->
CErrors.anomaly Pp.(str "[obligation_terminator] close_proof returned more than one proof term")
let obligation_hook prg obl num auto ctx' _ _ gr =
@@ -964,9 +964,9 @@ 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 ?hook guard =
+ let terminator guard =
Lemmas.Internal.make_terminator
- (obligation_terminator prg.prg_name num guard ?hook auto) in
+ (obligation_terminator prg.prg_name num guard auto) in
let hook = Lemmas.mk_hook (obligation_hook prg obl num auto) in
let lemma = Lemmas.start_lemma ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator ~hook in
let lemma = fst @@ Lemmas.by !default_tactic lemma in
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index f1c8b29313..8d1d9abc0b 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -22,7 +22,7 @@ val vernac_require :
(** The main interpretation function of vernacular expressions *)
val interp :
?verbosely:bool ->
- ?proof:(Proof_global.proof_object * Lemmas.proof_terminator) ->
+ ?proof:(Proof_global.proof_object * Lemmas.proof_terminator * Lemmas.declaration_hook option) ->
st:Vernacstate.t -> Vernacexpr.vernac_control -> Vernacstate.t
(** Prepare a "match" template for a given inductive type.
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index c51d3c30f4..0cdf748ce9 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -131,18 +131,18 @@ module Proof_global = struct
s_lemmas := Some stack;
res
- type closed_proof = Proof_global.proof_object * Lemmas.proof_terminator
+ type closed_proof = Proof_global.proof_object * Lemmas.proof_terminator * Lemmas.declaration_hook option
let return_proof ?allow_partial () = cc (return_proof ?allow_partial)
let close_future_proof ~opaque ~feedback_id pf =
cc_lemma (fun pt -> pf_fold (fun st -> close_future_proof ~opaque ~feedback_id st pf) pt,
- Internal.get_terminator pt)
+ Internal.get_terminator pt, Internal.get_hook pt)
let close_proof ~opaque ~keep_body_ucst_separate f =
cc_lemma (fun pt -> pf_fold ((close_proof ~opaque ~keep_body_ucst_separate f)) pt,
- Internal.get_terminator pt)
+ Internal.get_terminator pt, Internal.get_hook pt)
let discard_all () = s_lemmas := None
let update_global_env () = dd (update_global_env)
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index 9f4e366e1c..15b8aaefb6 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -51,7 +51,7 @@ module Proof_global : sig
val return_proof : ?allow_partial:bool -> unit -> Proof_global.closed_proof_output
- type closed_proof = Proof_global.proof_object * Lemmas.proof_terminator
+ type closed_proof = Proof_global.proof_object * Lemmas.proof_terminator * Lemmas.declaration_hook option
val close_future_proof :
opaque:Proof_global.opacity_flag ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:50:31 +0000