diff options
| author | Emilio Jesus Gallego Arias | 2019-02-24 01:57:59 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-17 12:30:13 +0200 |
| commit | a2ea73d84be2fe95eeda42f5f5ac458f0af9968f (patch) | |
| tree | 0b3c485f6e196bb74dca8c2eda6a6cf2448b2745 /vernac/vernacstate.ml | |
| parent | 5d18dfed8e68dd964bca5d64ca6bdd9f8ffbb1df (diff) | |
[proofs] Store hooks in the proof object.
As of now, hooks were stored in the terminators as closures, we place
them instead in the proof object and are thus passed back at proof
closing time.
This helps towards the reification and unification of terminators.
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) |