Proof_global: Simpler API for proof_terminator

3 files changed, 22 insertions, 22 deletions

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 6e3d8f7537..002810cdab 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
 
 (**********************************************************)
 (*                                                        *)
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 0519ac92bf..0635f03d03 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -64,9 +64,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
 
 (** [start_proof id str goals terminator] starts a proof of name [id]
     with goals [goals] (a list of pairs of environment and
@@ -74,19 +73,15 @@ type closed_proof = proof_object*proof_terminator Ephemeron.key
     is (spiwack: for potential printing, I believe is used only by
     closing commands and the xml plugin); [terminator] is used at the
     end of the proof to close the proof. *)
-val start_proof : Names.Id.t ->
-                          Decl_kinds.goal_kind ->
-                          (Environ.env * Term.types) list  ->
-                          proof_terminator ->
-                          unit
+val start_proof :
+  Names.Id.t -> Decl_kinds.goal_kind -> (Environ.env * Term.types) list  ->
+    proof_terminator -> unit
+
 (** Like [start_proof] except that there may be dependencies between
     initial goals. *)
-val start_dependent_proof : Names.Id.t ->
-                          Decl_kinds.goal_kind ->
-                          Proofview.telescope  ->
-                          proof_terminator ->
-                          unit
-
+val start_dependent_proof :
+  Names.Id.t -> Decl_kinds.goal_kind -> Proofview.telescope  ->
+    proof_terminator -> unit
 
 (* Takes a function to add to the exceptions data relative to the
    state in which the proof was built *)
@@ -101,7 +96,8 @@ val close_future_proof : feedback_id:Stateid.t ->
 
 (** 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
+val get_terminator : unit -> proof_terminator
+val set_terminator : proof_terminator -> unit
 
 exception NoSuchProof
 
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index 1421aaeed2..ac0dac03f1 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -404,7 +404,7 @@ let start_proof_com kind thms hook =
 
 let save_proof ?proof = function
   | Vernacexpr.Admitted ->
-      Ephemeron.get (Proof_global.get_terminator()) Proof_global.Admitted
+      Proof_global.get_terminator() Proof_global.Admitted
   | Vernacexpr.Proved (is_opaque,idopt) ->
       let (proof_obj,terminator) =
         match proof with
@@ -413,7 +413,7 @@ let save_proof ?proof = function
       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))
+      terminator (Proof_global.Proved (is_opaque,idopt,proof_obj))
 
 (* Miscellaneous *)