diff options
Diffstat (limited to 'vernac/vernacstate.ml')
| -rw-r--r-- | vernac/vernacstate.ml | 6 |
1 files changed, 3 insertions, 3 deletions
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) |