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.mli | |
| 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.mli')
| -rw-r--r-- | vernac/vernacstate.mli | 2 |
1 files changed, 1 insertions, 1 deletions
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 -> |