diff options
| -rw-r--r-- | proofs/proof_global.ml | 10 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 10 | ||||
| -rw-r--r-- | toplevel/lemmas.ml | 27 |
3 files changed, 33 insertions, 14 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 1ed63511d..5da216122 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 0000fe974..a8f2f2720 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 diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml index b0c04556f..5da651120 100644 --- a/toplevel/lemmas.ml +++ b/toplevel/lemmas.ml @@ -307,11 +307,11 @@ let get_proof proof do_guard hook opacity = let start_proof id kind ?sign c ?init_tac ?(compute_guard=[]) hook = let hook = Ephemeron.create hook in - let terminator = let open Vernacexpr in function - | Admitted,_ -> + let terminator = let open Proof_global in function + | Admitted -> admit hook (); Pp.feedback Interface.AddedAxiom - | Proved (is_opaque,idopt),proof -> + | Proved (is_opaque,idopt,proof) -> let proof = get_proof proof compute_guard hook is_opaque in begin match idopt with | None -> save_named proof @@ -400,15 +400,18 @@ let start_proof_com kind thms hook = (* Saving a proof *) -let save_proof ?proof ending = - let (proof_obj,terminator) = - match proof with - | None -> Proof_global.close_proof (fun x -> x) - | Some proof -> proof - in - (* if the proof is given explicitly, nothing has to be deleted *) - if Option.is_empty proof then Pfedit.delete_current_proof (); - Ephemeron.get terminator (ending,proof_obj) +let save_proof ?proof = function + | Vernacexpr.Admitted -> + Ephemeron.get (Proof_global.get_terminator()) Proof_global.Admitted + | Vernacexpr.Proved (is_opaque,idopt) -> + let (proof_obj,terminator) = + match proof with + | None -> Proof_global.close_proof (fun x -> x) + | Some proof -> proof + in + (* if the proof is given explicitly, nothing has to be deleted *) + if Option.is_empty proof then Pfedit.delete_current_proof (); + Ephemeron.get terminator (Proof_global.Proved (is_opaque,idopt,proof_obj)) (* Miscellaneous *) |