Opacifying the proof_terminator type.

5 files changed, 15 insertions, 5 deletions

diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index c232ae31a..96d5279a7 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -93,6 +93,7 @@ let start_deriving f suchthat lemma =
       ignore (Declare.declare_constant lemma lemma_def)
       in
 
+  let terminator = Proof_global.make_terminator terminator in
   let () = Proof_global.start_dependent_proof lemma kind goals terminator in
   let _ = Proof_global.with_current_proof begin fun _ p ->
     Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index d024c01ba..e48a336a6 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -134,7 +134,8 @@ let next = let n = ref 0 in fun () -> incr n; !n
 
 let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theorem) typ tac =
   let evd = Evd.from_env ~ctx Environ.empty_env in
-  start_proof id goal_kind evd sign typ (fun _ -> ());
+  let terminator = Proof_global.make_terminator (fun _ -> ()) in
+  start_proof id goal_kind evd sign typ terminator;
   try
     let status = by tac in
     let _,(const,univs,_) = cook_proof () in
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index c02b90916..10e7b758d 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -91,6 +91,9 @@ type pstate = {
   mode : proof_mode Ephemeron.key;
 }
 
+let make_terminator f = f
+let apply_terminator f = f
+
 (* The head of [!pstates] is the actual current proof, the other ones are
    to be resumed when the current proof is closed or aborted. *)
 let pstates = ref ([] : pstate list)
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index b5dd5ef85..995e90efc 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -70,9 +70,12 @@ 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 proof_terminator
 type closed_proof = proof_object * proof_terminator
 
+val make_terminator : (proof_ending -> unit) -> proof_terminator
+val apply_terminator : proof_terminator -> proof_ending -> unit
+
 (** [start_proof id str goals terminator] starts a proof of name [id]
     with goals [goals] (a list of pairs of environment and
     conclusion); [str] describes what kind of theorem/definition this
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index a7ef96c66..af4178eed 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -327,7 +327,8 @@ let check_exist =
   )
 
 let universe_proof_terminator compute_guard hook =
-  let open Proof_global in function
+  let open Proof_global in
+  make_terminator begin function
   | Admitted (id,k,pe,ctx) ->
       admit (id,k,pe) (hook (Some ctx)) ();
       Pp.feedback Feedback.AddedAxiom
@@ -345,6 +346,7 @@ let universe_proof_terminator compute_guard hook =
           save_anonymous_with_strength ~export_seff proof kind id
       end;
       check_exist exports
+  end
 
 let standard_proof_terminator compute_guard hook =
   universe_proof_terminator compute_guard (fun _ -> hook)
@@ -482,7 +484,7 @@ let save_proof ?proof = function
               | _ -> None in
             Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None),universes)
       in
-      Proof_global.get_terminator() pe
+      Proof_global.apply_terminator (Proof_global.get_terminator ()) pe
   | Vernacexpr.Proved (is_opaque,idopt) ->
       let (proof_obj,terminator) =
         match proof with
@@ -492,7 +494,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 ();
-      terminator (Proof_global.Proved (is_opaque,idopt,proof_obj))
+      Proof_global.(apply_terminator terminator (Proved (is_opaque,idopt,proof_obj)))
 
 (* Miscellaneous *)