diff options
| author | Arnaud Spiwack | 2013-12-02 15:09:00 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2013-12-04 14:14:33 +0100 |
| commit | 3c199b86ddf919d79ad79eb7d69f4b6f81bb73ab (patch) | |
| tree | 495418c4d20844e5001254c7169e1c158fdce3bc /proofs | |
| parent | 6d08c015517b59e68507d2caf72a11734293d613 (diff) | |
Fix Admitted.
Commit "The commands that initiate proofs…" was a bit hasty in its treatment of Admitted (in an attempt of making things simple, I actually required the proof to be completed for Admitted to go through…).
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proof_global.ml | 10 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 10 |
2 files changed, 18 insertions, 2 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 1ed63511da..5da2161222 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -71,7 +71,11 @@ type proof_object = { persistence : Decl_kinds.goal_kind; } -type proof_ending = Vernacexpr.proof_end * proof_object +type proof_ending = + | Admitted + | 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 @@ -331,6 +335,10 @@ let close_future_proof proof = close_proof ~now:false proof let close_proof fix_exn = close_proof ~now:true (Future.from_val ~fix_exn (return_proof ())) +(** Gets the current terminator without checking that the proof has + been completed. Useful for the likes of [Admitted]. *) +let get_terminator () = ( cur_pstate() ).terminator + (**********************************************************) (* *) (* Bullets *) diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 0000fe9744..a8f2f27202 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -59,7 +59,11 @@ type proof_object = { persistence : Decl_kinds.goal_kind; } -type proof_ending = Vernacexpr.proof_end * proof_object +type proof_ending = + | Admitted + | 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 @@ -95,6 +99,10 @@ val return_proof : unit -> Entries.proof_output list val close_future_proof : Entries.proof_output list Future.computation -> closed_proof +(** Gets the current terminator without checking that the proof has + been completed. Useful for the likes of [Admitted]. *) +val get_terminator : unit -> proof_terminator Ephemeron.key + exception NoSuchProof val get_open_goals : unit -> int |