[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.

1 files changed, 7 insertions, 4 deletions

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]