[save_proof] Make terminator API internal.

We refactor the terminator API to make it more internal. Indeed we
remove `set_terminator` and `get_terminator` is only there due to
access to internals in the STM `save_proof` path by the infamous
`?proof` parameter.

After this only 2 non-standard terminators remain: obligations and
derive. We will refactor those in next PRs.

7 files changed, 40 insertions, 34 deletions

diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index fd5b3a7e48..cff8214438 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -99,7 +99,7 @@ let start_deriving f suchthat name : Lemmas.t =
       ignore (Declare.declare_constant name lemma_def)
   in
 
-  let terminator ?hook _ = Lemmas.make_terminator terminator in
+  let terminator ?hook _ = Lemmas.Internal.make_terminator terminator in
   let lemma = Lemmas.start_dependent_lemma name kind goals ~terminator in
   Lemmas.simple_with_proof begin fun _ p ->
     Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p
diff --git a/stm/stm.ml b/stm/stm.ml
index a282efe265..20ad645ec5 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1673,14 +1673,17 @@ end = struct (* {{{ *)
         let _proof = PG_compat.return_proof ~allow_partial:true () in
         `OK_ADMITTED
       else begin
-      (* The original terminator, a hook, has not been saved in the .vio*)
-      PG_compat.set_terminator (Lemmas.standard_proof_terminator []);
-
       let opaque = Proof_global.Opaque in
-      let proof =
+
+      (* The original terminator, a hook, has not been saved in the .vio*)
+      let pterm, _invalid_terminator =
         PG_compat.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in
+
+      let proof = pterm , Lemmas.standard_proof_terminator [] in
+
       (* We jump at the beginning since the kernel handles side effects by also
        * looking at the ones that happen to be present in the current env *)
+
       Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:false start;
       (* STATE SPEC:
        * - start: First non-expired state! [This looks very fishy]
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 7e70de4209..160d933e50 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -54,15 +54,12 @@ type proof_ending =
               lident option *
               Proof_global.proof_object
 
-type proof_terminator = proof_ending -> unit
-
-let make_terminator f = f
-let apply_terminator f = f
+type proof_terminator = (proof_ending -> unit) CEphemeron.key
 
 (* Proofs with a save constant function *)
 type t =
   { proof : Proof_global.t
-  ; terminator : proof_terminator CEphemeron.key
+  ; terminator : proof_terminator
   }
 
 let pf_map f { proof; terminator} = { proof = f proof; terminator }
@@ -70,6 +67,18 @@ let pf_fold f ps = f ps.proof
 
 let set_endline_tactic t = pf_map (Proof_global.set_endline_tactic t)
 
+(* To be removed *)
+module Internal = struct
+
+let make_terminator f = CEphemeron.create f
+let apply_terminator f = CEphemeron.get f
+
+(** Gets the current terminator without checking that the proof has
+    been completed. Useful for the likes of [Admitted]. *)
+let get_terminator ps = ps.terminator
+
+end
+
 let with_proof f { proof; terminator } =
   let proof, res = Proof_global.with_proof f proof in
   { proof; terminator }, res
@@ -80,11 +89,6 @@ let by tac { proof; terminator } =
   let proof, res = Pfedit.by tac proof in
   { proof; terminator}, res
 
-(** Gets the current terminator without checking that the proof has
-    been completed. Useful for the likes of [Admitted]. *)
-let get_terminator ps = CEphemeron.get ps.terminator
-let set_terminator hook ps = { ps with terminator = CEphemeron.create hook }
-
 (* Support for mutually proved theorems *)
 
 let retrieve_first_recthm uctx = function
@@ -320,7 +324,7 @@ let admit ?hook ctx (id,k,e) pl () =
 
 let standard_proof_terminator ?(hook : declaration_hook option) compute_guard =
   let open Proof_global in
-  make_terminator begin function
+  CEphemeron.create begin function
   | Admitted (id,k,pe,ctx) ->
     let () = admit ?hook ctx (id,k,pe) (UState.universe_binders ctx) () in
     Feedback.feedback Feedback.AddedAxiom
@@ -393,7 +397,6 @@ let start_lemma id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c
   in
   let goals = [ Global.env_of_context sign , c ] in
   let proof = Proof_global.start_proof sigma id ?pl kind goals in
-  let terminator = CEphemeron.create terminator in
   { proof ; terminator }
 
 let start_dependent_lemma id ?pl kind ?terminator ?sign ?(compute_guard=[]) ?hook telescope =
@@ -402,7 +405,6 @@ let start_dependent_lemma id ?pl kind ?terminator ?sign ?(compute_guard=[]) ?hoo
   | Some terminator -> terminator ?hook compute_guard
   in
   let proof = Proof_global.start_dependent_proof id ?pl kind telescope in
-  let terminator = CEphemeron.create terminator in
   { proof ; terminator }
 
 let rec_tac_initializer finite guard thms snl =
@@ -560,7 +562,7 @@ let save_lemma_proved ?proof ?lemma ~opaque ~idopt =
       (* XXX: The close_proof and proof state API should be refactored
          so it is possible to insert proofs properly into the state *)
       let { proof; terminator } = Option.get lemma in
-      Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) proof, CEphemeron.get terminator
+      Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) proof, terminator
     | Some proof -> proof
   in
-  terminator (Proved (opaque,idopt,proof_obj))
+  CEphemeron.get terminator (Proved (opaque,idopt,proof_obj))
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 2c51095786..9afcd9a7ce 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -149,7 +149,14 @@ type proof_ending =
               Names.lident option *
               Proof_global.proof_object
 
-val make_terminator : (proof_ending -> unit) -> proof_terminator
-val apply_terminator : proof_terminator -> proof_ending -> unit
-val get_terminator : t -> proof_terminator
-val set_terminator : proof_terminator -> t -> t
+(** This stuff is internal and will be removed in the future.  *)
+module Internal : sig
+
+  (** Only needed due to the Proof_global compatibility layer. *)
+  val get_terminator : t -> proof_terminator
+
+  (** Only needed by obligations, should be reified soon *)
+  val make_terminator : (proof_ending -> unit) -> proof_terminator
+  val apply_terminator : proof_terminator -> proof_ending -> unit
+
+end
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index f1286e2f1f..6c9ec95c5f 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -844,7 +844,7 @@ let obligation_terminator ?hook name num guard auto pf =
   let open Lemmas in
   let term = standard_proof_terminator ?hook guard in
   match pf with
-  | Admitted _ -> apply_terminator term pf
+  | Admitted _ -> Internal.apply_terminator term pf
   | Proved (opq, id, { entries=[entry]; universes=uctx } ) -> begin
     let env = Global.env () in
     let ty = entry.Entries.const_entry_type in
@@ -965,7 +965,7 @@ let rec solve_obligation prg num tac =
   let evd = Evd.update_sigma_env evd (Global.env ()) in
   let auto n tac oblset = auto_solve_obligations n ~oblset tac in
   let terminator ?hook guard =
-    Lemmas.make_terminator
+    Lemmas.Internal.make_terminator
       (obligation_terminator prg.prg_name num guard ?hook auto) in
   let hook = Lemmas.mk_hook (obligation_hook prg obl num auto) in
   let lemma = Lemmas.start_lemma ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator ~hook in
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index 90075cbb70..af68ef88cf 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -114,14 +114,9 @@ module Proof_global = struct
     | None -> raise NoCurrentProof
     | Some x -> s_lemmas := Some (Stack.map_top_pstate ~f x)
 
-  let dd_lemma f = match !s_lemmas with
-    | None -> raise NoCurrentProof
-    | Some x -> s_lemmas := Some (Stack.map_top ~f x)
-
   let there_are_pending_proofs () = !s_lemmas <> None
   let get_open_goals () = cc get_open_goals
 
-  let set_terminator x = dd_lemma (set_terminator x)
   let give_me_the_proof_opt () = Option.map (Stack.with_top_pstate ~f:get_proof) !s_lemmas
   let give_me_the_proof () = cc get_proof
   let get_current_proof_name () = cc get_proof_name
@@ -143,11 +138,11 @@ module Proof_global = struct
 
   let close_future_proof ~opaque ~feedback_id pf =
     cc_lemma (fun pt -> pf_fold (fun st -> close_future_proof ~opaque ~feedback_id st pf) pt,
-                        get_terminator pt)
+                        Internal.get_terminator pt)
 
   let close_proof ~opaque ~keep_body_ucst_separate f =
     cc_lemma (fun pt -> pf_fold ((close_proof ~opaque ~keep_body_ucst_separate f)) pt,
-                        get_terminator pt)
+                        Internal.get_terminator pt)
 
   let discard_all () = s_lemmas := None
   let update_global_env () = dd (update_global_env)
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index 1bb18116b5..bfa85e022c 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -41,7 +41,6 @@ module Proof_global : sig
   val there_are_pending_proofs : unit -> bool
   val get_open_goals : unit -> int
 
-  val set_terminator : Lemmas.proof_terminator -> unit
   val give_me_the_proof : unit -> Proof.t
   val give_me_the_proof_opt : unit -> Proof.t option
   val get_current_proof_name : unit -> Names.Id.t