diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2013-12-26 11:19:19 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-01-04 17:07:15 +0100 |
| commit | 0a6227fe2ccb3f7012aad1b477e7b3f6b9c24da3 (patch) | |
| tree | 173461a164155dccbe5d3ef07c875367f5c459c3 /proofs/proof_global.ml | |
| parent | f21fa7e0c205417925e6bf9e563dbb7181fe6bd2 (diff) | |
Proof_global: Simpler API for proof_terminator
Diffstat (limited to 'proofs/proof_global.ml')
| -rw-r--r-- | proofs/proof_global.ml | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 6e3d8f753..002810cda 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -76,9 +76,8 @@ type proof_ending = | Proved of Vernacexpr.opacity_flag * (Vernacexpr.lident * Decl_kinds.theorem_kind option) option * proof_object -type proof_terminator = - proof_ending -> unit -type closed_proof = proof_object*proof_terminator Ephemeron.key +type proof_terminator = proof_ending -> unit +type closed_proof = proof_object * proof_terminator type pstate = { pid : Id.t; @@ -303,7 +302,8 @@ let close_proof ?feedback_id ~now fpl = fpl initial_goals in if now then List.iter (fun x -> ignore(Future.join x.Entries.const_entry_body)) entries; - { id = pid; entries = entries; persistence = strength }, terminator + { id = pid; entries = entries; persistence = strength }, + Ephemeron.get terminator let return_proof () = let { proof } = cur_pstate () in @@ -333,7 +333,11 @@ let close_proof fix_exn = (** Gets the current terminator without checking that the proof has been completed. Useful for the likes of [Admitted]. *) -let get_terminator () = ( cur_pstate() ).terminator +let get_terminator () = Ephemeron.get ( cur_pstate() ).terminator +let set_terminator hook = + match !pstates with + | [] -> raise NoCurrentProof + | p :: ps -> pstates := { p with terminator = Ephemeron.create hook } :: ps (**********************************************************) (* *) |