Proof_global: pass only 1 pstate when we don't want the proof stack

Typically instead of [start_proof : ontop:Proof_global.t option -> bla ->
Proof_global.t] we have [start_proof : bla -> Proof_global.pstate] and
the pstate is pushed on the stack by a caller around the
vernacentries/mlg level.

Naming can be a bit awkward, hopefully it can be improved (maybe in a
followup PR).

We can see some patterns appear waiting for nicer combinators, eg in
mlg we often only want to work with the current proof, not the stack.

Behaviour should be similar modulo bugs, let's see what CI says.

5 files changed, 9 insertions, 8 deletions

diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 4c186dce09..5e4969567d 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -1118,7 +1118,7 @@ END
 
 VERNAC COMMAND EXTEND OptimizeProof
 | ![ proof ] [ "Optimize" "Proof" ] => { classify_as_proofstep } ->
-  { fun ~pstate -> Option.map Proof_global.compact_the_proof pstate }
+  { fun ~pstate -> Option.map Proof_global.(modify_current_pstate compact_the_proof) pstate }
 | [ "Optimize" "Heap" ] => { classify_as_proofstep } ->
   { Gc.compact () }
 END
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index de3a9c9fa9..d7918a58ac 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -80,8 +80,8 @@ GRAMMAR EXTEND Gram
 
 open Obligations
 
-let obligation ~pstate obl tac = Some (with_tac (fun t -> Obligations.obligation ~ontop:pstate obl t) tac)
-let next_obligation ~pstate obl tac = Some (with_tac (fun t -> Obligations.next_obligation ~ontop:pstate obl t) tac)
+let obligation ~pstate obl tac = Some (Proof_global.push ~ontop:pstate (with_tac (fun t -> Obligations.obligation obl t) tac))
+let next_obligation ~pstate obl tac = Some (Proof_global.push ~ontop:pstate (with_tac (fun t -> Obligations.next_obligation obl t) tac))
 
 let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]), VtLater)
 
diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index 2fad1f6b6a..e3f4b8ef59 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -280,7 +280,8 @@ VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF
     (* This command may or may not open a goal *)
     => { (if Lib.is_modtype() then VtSideff([n]) else VtStartProof(GuaranteesOpacity, [n])), VtLater }
     -> {
-          add_morphism_infer atts m n
+      fun ~pstate:ontop ->
+        Option.cata (fun ps -> Some (Proof_global.push ~ontop ps)) ontop (add_morphism_infer atts m n)
        }
   | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ]
     => { VtStartProof(GuaranteesOpacity,[n]), VtLater }
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 6f84e6c18d..efca411754 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1974,7 +1974,7 @@ let warn_add_morphism_deprecated =
   CWarnings.create ~name:"add-morphism" ~category:"deprecated" (fun () ->
       Pp.(str "Add Morphism f : id is deprecated, please use Add Morphism f with signature (...) as id"))
 
-let add_morphism_infer ~pstate atts m n : Proof_global.t option =
+let add_morphism_infer atts m n : Proof_global.pstate option =
   warn_add_morphism_deprecated ?loc:m.CAst.loc ();
   init_setoid ();
   let instance_id = add_suffix n "_Proper" in
@@ -1991,7 +1991,7 @@ let add_morphism_infer ~pstate atts m n : Proof_global.t option =
       add_instance (Classes.mk_instance
                       (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (ConstRef cst));
       declare_projection n instance_id (ConstRef cst);
-      pstate
+      None
     else
       let kind = Decl_kinds.Global, atts.polymorphic,
                  Decl_kinds.DefinitionBody Decl_kinds.Instance
@@ -2008,7 +2008,7 @@ let add_morphism_infer ~pstate atts m n : Proof_global.t option =
       let hook = Lemmas.mk_hook hook in
       Flags.silently
         (fun () ->
-           let pstate = Lemmas.start_proof ~ontop:pstate ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in
+           let pstate = Lemmas.start_proof ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in
            Some (fst Pfedit.(by (Tacinterp.interp tac) pstate))) ()
 
 let add_morphism ~pstate atts binders m s n =
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index a200cb5ced..cab7d0065e 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -89,7 +89,7 @@ val add_setoid : pstate:Proof_global.t option ->
   rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> constr_expr ->
   Id.t -> Proof_global.t option
 
-val add_morphism_infer : pstate:Proof_global.t option -> rewrite_attributes -> constr_expr -> Id.t -> Proof_global.t option
+val add_morphism_infer : rewrite_attributes -> constr_expr -> Id.t -> Proof_global.pstate option
 
 val add_morphism : pstate:Proof_global.t option ->
   rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> Proof_global.t option