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…).

3 files changed, 33 insertions, 14 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
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index b0c04556fb..5da651120d 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 *)