coqpp: add new ![] specifiers for structured proof interaction

![proof_stack] is equivalent to the old meaning of ![proof]: the body
has type `pstate:Proof_global.t option -> Proof_global.t option`

The other specifiers are for the following body types:

~~~
![open_proof] `is_ontop:bool -> pstate`

![maybe_open_proof] `is_ontop:bool -> pstate option`

![proof] `pstate:pstate -> pstate`

![proof_opt_query] `pstate:pstate option -> unit`

![proof_query] `pstate:pstate -> unit`
~~~

The `is_ontop` is only used for the warning message when declaring a
section variable inside a proof, we could also just stop warning.

The specifiers look closely related to stm classifiers, but currently
they're unconnected. Notably this means that a ![proof_query] doesn't
have to be classified QUERY.

![proof_stack] is only used by g_rewrite/rewrite whose behaviour I
 don't fully understand, maybe we can drop it in the future.

For compat we may want to consider keeping ![proof] with its old
meaning and using some new name for the new meaning. OTOH fixing
plugins to be stricter is easier if we change it as the errors tell us
where it's used.

23 files changed, 188 insertions, 173 deletions

diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index 42fe13e4eb..8444f3a58c 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -359,10 +359,29 @@ let print_atts_right fmt = function
 
 let print_body_wrapper fmt r =
   match r.vernac_state with
-  | Some "proof" ->
+  | Some "proof_stack" ->
     fprintf fmt "let proof = (%a) ~pstate:st.Vernacstate.proof in { st with Vernacstate.proof }" print_code r.vernac_body
+
+  | Some "open_proof" ->
+    let push = "Some (Proof_global.push ~ontop:st.Vernacstate.proof pstate)" in
+    fprintf fmt "let pstate = (%a) in let proof = %s in { st with Vernacstate.proof }" print_code r.vernac_body push
+
+  | Some "maybe_open_proof" ->
+    let push = "Proof_global.maybe_push ~ontop:st.Vernacstate.proof pstate" in
+    fprintf fmt "let pstate = (%a) in let proof = %s in { st with Vernacstate.proof }" print_code r.vernac_body push
+
+  | Some "proof" ->
+    fprintf fmt "let proof = Vernacentries.modify_pstate ~pstate:st.Vernacstate.proof (%a) in { st with Vernacstate.proof }" print_code r.vernac_body
+
+  | Some "proof_opt_query" ->
+    fprintf fmt "let () = (%a) ~pstate:(Vernacstate.pstate st) in st" print_code r.vernac_body
+
+  | Some "proof_query" ->
+    fprintf fmt "let () = Vernacentries.with_pstate ~pstate:st.Vernacstate.proof (%a) in st" print_code r.vernac_body
+
   | None ->
     fprintf fmt "let () = %a in st" print_code r.vernac_body
+
   | Some x ->
     fatal ("unsupported state specifier: " ^ x)
 
diff --git a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
index 147b0df567..300d62285a 100644
--- a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
+++ b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
@@ -145,13 +145,11 @@ END
   it gives an error message that is basically impossible to understand. *)
 
 VERNAC COMMAND EXTEND ExploreProof CLASSIFIED AS QUERY
-| ![ proof ] [ "Cmd9" ] ->
-  { fun ~pstate:ontop ->
-    Option.iter (fun ontop ->
-        let pstate = Proof_global.get_current_pstate ontop in
-        let sigma, env = Pfedit.get_current_context pstate in
-        let pprf = Proof.partial_proof Proof_global.(give_me_the_proof pstate) in
-        Feedback.msg_notice
-          (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf)) ontop;
-    ontop }
+| ![ proof_query ] [ "Cmd9" ] ->
+  { fun ~pstate ->
+    let sigma, env = Pfedit.get_current_context pstate in
+    let pprf = Proof.partial_proof Proof_global.(give_me_the_proof pstate) in
+    Feedback.msg_notice
+      (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf)
+  }
 END
diff --git a/plugins/derive/g_derive.mlg b/plugins/derive/g_derive.mlg
index ee076f5ae3..d25b8fd01c 100644
--- a/plugins/derive/g_derive.mlg
+++ b/plugins/derive/g_derive.mlg
@@ -23,6 +23,6 @@ let classify_derive_command _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpac
 }
 
 VERNAC COMMAND EXTEND Derive CLASSIFIED BY { classify_derive_command }
-| ![ proof ] [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] ->
-  { fun ~pstate -> Some (Proof_global.push ~ontop:pstate Derive.(start_deriving f suchthat lemma)) }
+| ![ open_proof ] [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] ->
+  { Derive.(start_deriving f suchthat lemma) }
 END
diff --git a/plugins/extraction/g_extraction.mlg b/plugins/extraction/g_extraction.mlg
index d43d90af60..487accbc9b 100644
--- a/plugins/extraction/g_extraction.mlg
+++ b/plugins/extraction/g_extraction.mlg
@@ -178,12 +178,6 @@ END
 (* Show the extraction of the current proof *)
 
 VERNAC COMMAND EXTEND ShowExtraction CLASSIFIED AS QUERY
-| ![ proof ] [ "Show" "Extraction" ]
-  -> { fun ~pstate:ontop ->
-    let pstate = Option.map Proof_global.get_current_pstate ontop in
-    let pstate = match pstate with
-      | None -> CErrors.user_err Pp.(str "No ongoing proof")
-      | Some pstate -> pstate
-    in
-    let () = show_extraction ~pstate in ontop }
+| ![ proof_query ] [ "Show" "Extraction" ]
+  -> { show_extraction }
 END
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index b8db3dc5ce..cc772e96f3 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -177,7 +177,7 @@ let () =
 
 (* TASSI: n'importe quoi ! *)
 VERNAC COMMAND EXTEND Function
-| ![ proof ] ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")]
+| ![ maybe_open_proof ] ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")]
     => { let hard = List.exists (function
            | _,((_,(Some { CAst.v = CMeasureRec _ }
              | Some { CAst.v = CWfRec _}),_,_,_),_) -> true
@@ -190,9 +190,7 @@ VERNAC COMMAND EXTEND Function
          | Vernacextend.VtSideff ids, _ when hard ->
              Vernacextend.(VtStartProof (GuaranteesOpacity, ids), VtLater)
          | x -> x }
-    -> { fun ~pstate:ontop ->
-      let pstate = do_generate_principle false (List.map snd recsl) in
-      Proof_global.maybe_push ~ontop pstate}
+    -> { do_generate_principle false (List.map snd recsl) }
 END
 
 {
@@ -227,33 +225,32 @@ let warning_error names e =
 }
 
 VERNAC COMMAND EXTEND NewFunctionalScheme
-| ![ proof ] ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ]
+| ![ maybe_open_proof ] ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ]
    => { Vernacextend.(VtSideff(List.map pi1 fas), VtLater) }
    ->
-    { fun ~pstate:ontop ->
-      begin
+    { begin
         try
-          Functional_principles_types.build_scheme fas; ontop
+          Functional_principles_types.build_scheme fas; None
         with
         | Functional_principles_types.No_graph_found ->
           begin
             match fas with
             | (_,fun_name,_)::_ ->
               begin
-                let ontop = make_graph ~ontop (Smartlocate.global_with_alias fun_name) in
-                try Functional_principles_types.build_scheme fas; ontop
+                let pstate = make_graph (Smartlocate.global_with_alias fun_name) in
+                try Functional_principles_types.build_scheme fas; pstate
                 with
                 | Functional_principles_types.No_graph_found ->
                   CErrors.user_err Pp.(str "Cannot generate induction principle(s)")
                 | e when CErrors.noncritical e ->
                   let names = List.map (fun (_,na,_) -> na) fas in
-                  warning_error names e; ontop
+                  warning_error names e; pstate
               end
 	      | _ -> assert false (* we can only have non empty  list *)
           end
         | e when CErrors.noncritical e ->
           let names = List.map (fun (_,na,_) -> na) fas in
-          warning_error names e; ontop
+          warning_error names e; None
       end
     }
 END
@@ -267,6 +264,6 @@ END
 
 (***** debug only ***)
 VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY
-| ![ proof ] ["Generate" "graph" "for" reference(c)] ->
-  { fun ~pstate:ontop -> make_graph ~ontop (Smartlocate.global_with_alias c) }
+| ![ maybe_open_proof ] ["Generate" "graph" "for" reference(c)] ->
+  { make_graph (Smartlocate.global_with_alias c) }
 END
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index d47c12a7cb..6ea2eb579f 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -839,7 +839,9 @@ let rec get_args b t : Constrexpr.local_binder_expr list *
     | _ -> [],b,t
 
 
-let make_graph env sigma (f_ref : GlobRef.t) =
+let make_graph (f_ref : GlobRef.t) =
+  let env = Global.env() in
+  let sigma = Evd.from_env env in
   let c,c_body =
     match f_ref with
     | ConstRef c ->
@@ -907,11 +909,4 @@ let make_graph env sigma (f_ref : GlobRef.t) =
            expr_list;
          pstate)
 
-let make_graph ~ontop f_ref =
-  let pstate = Option.map Proof_global.get_current_pstate ontop in
-  let sigma, env = Option.cata Pfedit.get_current_context
-      (let e = Global.env () in Evd.from_env e, e) pstate in
-  Option.cata (fun ps -> Some (Proof_global.push ~ontop ps)) ontop
-    (make_graph env sigma f_ref)
-
 let do_generate_principle = do_generate_principle [] warning_error true
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index cf4ef23d1a..c803484617 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -17,4 +17,4 @@ val functional_induction :
   Ltac_plugin.Tacexpr.or_and_intro_pattern option ->
   Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
 
-val make_graph : ontop:Proof_global.t option -> GlobRef.t -> Proof_global.t option
+val make_graph : GlobRef.t -> Proof_global.pstate option
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 5e4969567d..4a2fb425ac 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -934,7 +934,7 @@ END
 VERNAC COMMAND EXTEND GrabEvars
 | ![ proof ] [ "Grab" "Existential" "Variables" ]
   => { classify_as_proofstep }
-  -> { fun ~pstate -> Option.map (Proof_global.simple_with_current_proof (fun _ p  -> Proof.V82.grab_evars p)) pstate }
+  -> { fun ~pstate -> Proof_global.modify_proof (fun p  -> Proof.V82.grab_evars p) pstate }
 END
 
 (* Shelves all the goals under focus. *)
@@ -966,7 +966,7 @@ END
 VERNAC COMMAND EXTEND Unshelve
 | ![ proof ] [ "Unshelve" ]
   => { classify_as_proofstep }
-  -> { fun ~pstate -> Option.map (Proof_global.simple_with_current_proof (fun _ p  -> Proof.unshelve p)) pstate  }
+  -> { fun ~pstate -> Proof_global.modify_proof (fun p  -> Proof.unshelve p) pstate  }
 END
 
 (* Gives up on the goals under focus: the goals are considered solved,
@@ -1118,7 +1118,7 @@ END
 
 VERNAC COMMAND EXTEND OptimizeProof
 | ![ proof ] [ "Optimize" "Proof" ] => { classify_as_proofstep } ->
-  { fun ~pstate -> Option.map Proof_global.(modify_current_pstate compact_the_proof) pstate }
+  { fun ~pstate -> Proof_global.compact_the_proof pstate }
 | [ "Optimize" "Heap" ] => { classify_as_proofstep } ->
   { Gc.compact () }
 END
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 7eb34158e8..9bf5bd1bda 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -376,7 +376,7 @@ let () = declare_int_option {
 
 let vernac_solve ~pstate n info tcom b =
   let open Goal_select in
-  let pstate, status = Proof_global.with_current_proof (fun etac p ->
+  let pstate, status = Proof_global.with_proof (fun etac p ->
       let with_end_tac = if b then Some etac else None in
       let global = match n with SelectAll | SelectList _ -> true | _ -> false in
       let info = Option.append info !print_info_trace in
@@ -388,7 +388,7 @@ let vernac_solve ~pstate n info tcom b =
       let p = Proof.maximal_unfocus Vernacentries.command_focus p in
       p,status) pstate in
   if not status then Feedback.feedback Feedback.AddedAxiom;
-  Some pstate
+  pstate
 
 let pr_ltac_selector s = Pptactic.pr_goal_selector ~toplevel:true s
 
@@ -438,7 +438,7 @@ VERNAC { tactic_mode } EXTEND VernacSolve
 | ![ proof ] [ ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
     { classify_as_proofstep } -> {
     let g = Option.default (Goal_select.get_default_goal_selector ()) g in
-    Vernacentries.vernac_require_open_proof vernac_solve g n t def
+    vernac_solve g n t def
   }
 | ![ proof ] [ "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
     {
@@ -450,7 +450,7 @@ VERNAC { tactic_mode } EXTEND VernacSolve
       VtLater
     } -> {
       let t = rm_abstract t in
-      Vernacentries.vernac_require_open_proof vernac_solve Goal_select.SelectAll n t def
+      vernac_solve Goal_select.SelectAll n t def
     }
 END
 
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index d7918a58ac..c01b97c14d 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -80,25 +80,25 @@ GRAMMAR EXTEND Gram
 
 open Obligations
 
-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 obligation obl tac = with_tac (fun t -> Obligations.obligation obl t) tac
+let next_obligation obl tac = with_tac (fun t -> Obligations.next_obligation obl t) tac
 
 let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]), VtLater)
 
 }
 
 VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl }
-| ![ proof ] [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] ->
+| ![ open_proof ] [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] ->
     { obligation (num, Some name, Some t) tac }
-| ![ proof ] [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] ->
+| ![ open_proof ] [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] ->
     { obligation (num, Some name, None) tac }
-| ![ proof ] [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] ->
+| ![ open_proof ] [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] ->
     { obligation (num, None, Some t) tac }
-| ![ proof ] [ "Obligation" integer(num) withtac(tac) ] ->
+| ![ open_proof ] [ "Obligation" integer(num) withtac(tac) ] ->
     { obligation (num, None, None) tac }
-| ![ proof ] [ "Next" "Obligation" "of" ident(name) withtac(tac) ] ->
+| ![ open_proof ] [ "Next" "Obligation" "of" ident(name) withtac(tac) ] ->
     { next_obligation (Some name) tac }
-| ![ proof ] [ "Next" "Obligation" withtac(tac) ] -> { next_obligation None tac }
+| ![ open_proof ] [ "Next" "Obligation" withtac(tac) ] -> { next_obligation None tac }
 END
 
 VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF
diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index e3f4b8ef59..bb29323858 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -180,34 +180,34 @@ TACTIC EXTEND setoid_rewrite
 END
 
 VERNAC COMMAND EXTEND AddRelation CLASSIFIED AS SIDEFF
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+  | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
         "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] ->
       { declare_relation atts a aeq n (Some lemma1) (Some lemma2) None }
 
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+  | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
         "as" ident(n) ] ->
       { declare_relation atts a aeq n (Some lemma1) None None }
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq)  "as" ident(n) ] ->
+  | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq)  "as" ident(n) ] ->
       { declare_relation atts a aeq n None None None }
 END
 
 VERNAC COMMAND EXTEND AddRelation2 CLASSIFIED AS SIDEFF
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
+  | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
       "as" ident(n) ] ->
       { declare_relation atts a aeq n None (Some lemma2) None }
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)  "as" ident(n) ] ->
+  | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)  "as" ident(n) ] ->
       { declare_relation atts a aeq n None (Some lemma2) (Some lemma3) }
 END
 
 VERNAC COMMAND EXTEND AddRelation3 CLASSIFIED AS SIDEFF
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+  | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
       "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
       { declare_relation atts a aeq n (Some lemma1) None (Some lemma3) }
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+  | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
       "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)
       "as" ident(n) ] ->
       { declare_relation atts a aeq n (Some lemma1) (Some lemma2) (Some lemma3) }
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
+  | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
         "as" ident(n) ] ->
       { declare_relation atts a aeq n None None (Some lemma3) }
 END
@@ -234,66 +234,59 @@ GRAMMAR EXTEND Gram
 END
 
 VERNAC COMMAND EXTEND AddParametricRelation CLASSIFIED AS SIDEFF
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
+  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
         "reflexivity" "proved" "by" constr(lemma1)
         "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] ->
       { declare_relation atts ~binders:b a aeq n (Some lemma1) (Some lemma2) None }
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
+  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
         "reflexivity" "proved" "by" constr(lemma1)
         "as" ident(n) ] ->
       { declare_relation atts ~binders:b a aeq n (Some lemma1) None None }
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)  "as" ident(n) ] ->
+  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)  "as" ident(n) ] ->
       { declare_relation atts ~binders:b a aeq n None None None }
 END
 
 VERNAC COMMAND EXTEND AddParametricRelation2 CLASSIFIED AS SIDEFF
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
+  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
       "as" ident(n) ] ->
       { declare_relation atts ~binders:b a aeq n None (Some lemma2) None }
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)  "as" ident(n) ] ->
+  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)  "as" ident(n) ] ->
       { declare_relation atts ~binders:b a aeq n None (Some lemma2) (Some lemma3) }
 END
 
 VERNAC COMMAND EXTEND AddParametricRelation3 CLASSIFIED AS SIDEFF
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
       "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
       { declare_relation atts ~binders:b a aeq n (Some lemma1) None (Some lemma3) }
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
       "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)
       "as" ident(n) ] ->
       { declare_relation atts ~binders:b a aeq n (Some lemma1) (Some lemma2) (Some lemma3) }
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
+  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
         "as" ident(n) ] ->
       { declare_relation atts ~binders:b a aeq n None None (Some lemma3) }
 END
 
 VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
+  | #[ atts = rewrite_attributes; ] [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
      {
          add_setoid atts [] a aeq t n
      }
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
+  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
      {
          add_setoid atts binders a aeq t n
      }
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Morphism" constr(m) ":" ident(n) ]
+  | #[ atts = rewrite_attributes; ] ![ maybe_open_proof ] [ "Add" "Morphism" constr(m) ":" ident(n) ]
     (* This command may or may not open a goal *)
     => { (if Lib.is_modtype() then VtSideff([n]) else VtStartProof(GuaranteesOpacity, [n])), VtLater }
-    -> {
-      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) ]
+    -> { add_morphism_infer atts m n }
+  | #[ atts = rewrite_attributes; ] ![ open_proof ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ]
     => { VtStartProof(GuaranteesOpacity,[n]), VtLater }
-    -> {
-          add_morphism atts [] m s n
-       }
-  | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
+    -> { add_morphism atts [] m s n }
+  | #[ atts = rewrite_attributes; ] ![ open_proof ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
         "with" "signature" lconstr(s) "as" ident(n) ]
     => { VtStartProof(GuaranteesOpacity,[n]), VtLater }
-    -> {
-          add_morphism atts binders m s n
-       }
+    -> { add_morphism atts binders m s n }
 END
 
 TACTIC EXTEND setoid_symmetry
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index efca411754..5d57a2f27f 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -23,7 +23,6 @@ open Tacticals.New
 open Tactics
 open Pretype_errors
 open Typeclasses
-open Classes
 open Constrexpr
 open Globnames
 open Evd
@@ -1795,17 +1794,17 @@ let declare_an_instance n s args =
 
 let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
 
-let anew_instance ~pstate atts binders (name,t) fields =
+let anew_instance atts binders (name,t) fields =
   let program_mode = atts.program in
-  let _id, pstate = new_instance ~pstate ~program_mode atts.polymorphic
+  let _id, proof = Classes.new_instance ~program_mode atts.polymorphic
       name binders t (Some (true, CAst.make @@ CRecord (fields)))
       ~global:atts.global ~generalize:false Hints.empty_hint_info
   in
-  pstate
+  assert (Option.is_empty proof) (* refine:false with term *)
 
-let declare_instance_refl ~pstate atts binders a aeq n lemma =
+let declare_instance_refl atts binders a aeq n lemma =
   let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive"
-  in anew_instance ~pstate atts binders instance
+  in anew_instance atts binders instance
        [(qualid_of_ident (Id.of_string "reflexivity"),lemma)]
 
 let declare_instance_sym atts binders a aeq n lemma =
@@ -1818,41 +1817,41 @@ let declare_instance_trans atts binders a aeq n lemma =
   in anew_instance atts binders instance
        [(qualid_of_ident (Id.of_string "transitivity"),lemma)]
 
-let declare_relation ~pstate atts ?(binders=[]) a aeq n refl symm trans =
+let declare_relation atts ?(binders=[]) a aeq n refl symm trans =
   init_setoid ();
   let instance = declare_instance a aeq (add_suffix n "_relation") "Coq.Classes.RelationClasses.RewriteRelation" in
-  let pstate = anew_instance ~pstate atts binders instance [] in
+  let () = anew_instance atts binders instance [] in
   match (refl,symm,trans) with
-    (None, None, None) -> pstate
+    (None, None, None) -> ()
   | (Some lemma1, None, None) ->
-    declare_instance_refl ~pstate atts binders a aeq n lemma1
+    declare_instance_refl atts binders a aeq n lemma1
   | (None, Some lemma2, None) ->
-    declare_instance_sym ~pstate atts binders a aeq n lemma2
+    declare_instance_sym atts binders a aeq n lemma2
   | (None, None, Some lemma3) ->
-    declare_instance_trans ~pstate atts binders a aeq n lemma3
+    declare_instance_trans atts binders a aeq n lemma3
   | (Some lemma1, Some lemma2, None) ->
-    let pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in
-    declare_instance_sym ~pstate atts binders a aeq n lemma2
+    let () = declare_instance_refl atts binders a aeq n lemma1 in
+    declare_instance_sym atts binders a aeq n lemma2
   | (Some lemma1, None, Some lemma3) ->
-    let pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in
-    let pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in
+    let () = declare_instance_refl atts binders a aeq n lemma1 in
+    let () = declare_instance_trans atts binders a aeq n lemma3 in
     let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" in
-    anew_instance ~pstate atts binders instance
+    anew_instance atts binders instance
       [(qualid_of_ident (Id.of_string "PreOrder_Reflexive"), lemma1);
        (qualid_of_ident (Id.of_string "PreOrder_Transitive"),lemma3)]
   | (None, Some lemma2, Some lemma3) ->
-    let pstate = declare_instance_sym ~pstate atts binders a aeq n lemma2 in
-    let pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in
+    let () = declare_instance_sym atts binders a aeq n lemma2 in
+    let () = declare_instance_trans atts binders a aeq n lemma3 in
     let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" in
-    anew_instance ~pstate atts binders instance
+    anew_instance atts binders instance
       [(qualid_of_ident (Id.of_string "PER_Symmetric"), lemma2);
        (qualid_of_ident (Id.of_string "PER_Transitive"),lemma3)]
   | (Some lemma1, Some lemma2, Some lemma3) ->
-    let pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in
-    let pstate = declare_instance_sym ~pstate atts binders a aeq n lemma2 in
-    let pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in
+    let () = declare_instance_refl atts binders a aeq n lemma1 in
+    let () = declare_instance_sym atts binders a aeq n lemma2 in
+    let () = declare_instance_trans atts binders a aeq n lemma3 in
     let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in
-    anew_instance ~pstate atts binders instance
+    anew_instance atts binders instance
       [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), lemma1);
        (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), lemma2);
        (qualid_of_ident (Id.of_string "Equivalence_Transitive"), lemma3)]
@@ -1951,15 +1950,15 @@ let warn_add_setoid_deprecated =
   CWarnings.create ~name:"add-setoid" ~category:"deprecated" (fun () ->
       Pp.(str "Add Setoid is deprecated, please use Add Parametric Relation."))
 
-let add_setoid ~pstate atts binders a aeq t n =
+let add_setoid atts binders a aeq t n =
   warn_add_setoid_deprecated ?loc:a.CAst.loc ();
   init_setoid ();
-  let pstate = declare_instance_refl ~pstate atts binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in
-  let pstate = declare_instance_sym ~pstate atts binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in
-  let pstate = declare_instance_trans ~pstate atts binders a aeq n (mkappc "Seq_trans" [a;aeq;t]) in
+  let () = declare_instance_refl atts binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in
+  let () = declare_instance_sym atts binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in
+  let () = declare_instance_trans atts binders a aeq n (mkappc "Seq_trans" [a;aeq;t]) in
   let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
   in
-  anew_instance ~pstate atts binders instance
+  anew_instance atts binders instance
     [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]);
      (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]);
      (qualid_of_ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])]
@@ -1988,7 +1987,7 @@ let add_morphism_infer atts m n : Proof_global.pstate option =
              (None,(instance,uctx),None),
            Decl_kinds.IsAssumption Decl_kinds.Logical)
       in
-      add_instance (Classes.mk_instance
+      Classes.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);
       None
@@ -1999,7 +1998,7 @@ let add_morphism_infer atts m n : Proof_global.pstate option =
       let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
       let hook _ _ _ = function
         | Globnames.ConstRef cst ->
-          add_instance (Classes.mk_instance
+          Classes.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)
@@ -2011,7 +2010,7 @@ let add_morphism_infer atts m n : Proof_global.pstate option =
            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 =
+let add_morphism atts binders m s n =
   init_setoid ();
   let instance_id = add_suffix n "_Proper" in
   let instance_name = (CAst.make @@ Name instance_id),None in
@@ -2021,12 +2020,12 @@ let add_morphism ~pstate atts binders m s n =
        [cHole; s; m])
   in
   let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
-  let _, pstate = new_instance ~pstate
+  let _, pstate = Classes.new_instance
       ~program_mode:atts.program ~global:atts.global atts.polymorphic
       instance_name binders instance_t None
       ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info
   in
-  pstate
+  Option.get pstate (* no instance body -> always open proof *)
 
 (** Bind to "rewrite" too *)
 
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index cab7d0065e..e1cbc46b3b 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -81,18 +81,35 @@ val cl_rewrite_clause :
 val is_applied_rewrite_relation :
   env -> evar_map -> rel_context -> constr -> types option
 
-val declare_relation : pstate:Proof_global.t option -> rewrite_attributes ->
-  ?binders:local_binder_expr list -> constr_expr -> constr_expr -> Id.t ->
-  constr_expr option -> constr_expr option -> constr_expr option -> Proof_global.t option
-
-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 declare_relation
+  : rewrite_attributes
+  -> ?binders:local_binder_expr list
+  -> constr_expr
+  -> constr_expr
+  -> Id.t
+  -> constr_expr option
+  -> constr_expr option
+  -> constr_expr option
+  -> unit
+
+val add_setoid
+  : rewrite_attributes
+  -> local_binder_expr list
+  -> constr_expr
+  -> constr_expr
+  -> constr_expr
+  -> Id.t
+  -> unit
 
 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
+val add_morphism
+  : rewrite_attributes
+  -> local_binder_expr list
+  -> constr_expr
+  -> constr_expr
+  -> Id.t
+  -> Proof_global.pstate
 
 val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr
 
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index 49c547a979..bd1f925486 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -90,7 +90,6 @@ let tac2def_typ = Entry.create "tactic:tac2def_typ"
 let tac2def_ext = Entry.create "tactic:tac2def_ext"
 let tac2def_syn = Entry.create "tactic:tac2def_syn"
 let tac2def_mut = Entry.create "tactic:tac2def_mut"
-let tac2def_run = Entry.create "tactic:tac2def_run"
 let tac2mode = Entry.create "vernac:ltac2_command"
 
 let ltac1_expr = Pltac.tactic_expr
@@ -114,7 +113,7 @@ let pattern_of_qualid qid =
 
 GRAMMAR EXTEND Gram
   GLOBAL: tac2expr tac2type tac2def_val tac2def_typ tac2def_ext tac2def_syn
-          tac2def_mut tac2def_run;
+          tac2def_mut;
   tac2pat:
     [ "1" LEFTA
       [ qid = Prim.qualid; pl = LIST1 tac2pat LEVEL "0" -> {
@@ -288,9 +287,6 @@ GRAMMAR EXTEND Gram
   tac2def_mut:
     [ [ "Set"; qid = Prim.qualid; ":="; e = tac2expr -> { StrMut (qid, e) } ] ]
   ;
-  tac2def_run:
-    [ [ "Eval"; e = tac2expr -> { StrRun e } ] ]
-  ;
   tac2typ_knd:
     [ [ t = tac2type -> { CTydDef (Some t) }
       | "["; ".."; "]" -> { CTydOpn }
@@ -878,20 +874,27 @@ PRINTED BY { pr_ltac2entry }
 | [ tac2def_ext(e) ] -> { e }
 | [ tac2def_syn(e) ] -> { e }
 | [ tac2def_mut(e) ] -> { e }
-| [ tac2def_run(e) ] -> { e }
+END
+
+VERNAC ARGUMENT EXTEND ltac2_expr
+PRINTED BY { pr_ltac2expr }
+| [ tac2expr(e) ] -> { e }
 END
 
 {
 
 let classify_ltac2 = function
 | StrSyn _ -> Vernacextend.(VtSideff [], VtNow)
-| StrMut _ | StrVal _ | StrPrm _  | StrTyp _ | StrRun _ -> Vernacextend.classify_as_sideeff
+| StrMut _ | StrVal _ | StrPrm _  | StrTyp _ -> Vernacextend.classify_as_sideeff
 
 }
 
 VERNAC COMMAND EXTEND VernacDeclareTactic2Definition
-| #[ local = locality ] ![proof] [ "Ltac2" ltac2_entry(e) ] => { classify_ltac2 e } -> {
-  fun ~pstate -> Tac2entries.register_struct ?local ~pstate:(Option.map Proof_global.get_current_pstate pstate) e; pstate
+| #[ local = locality ] [ "Ltac2" ltac2_entry(e) ] => { classify_ltac2 e } -> {
+  Tac2entries.register_struct ?local e
+  }
+| ![proof_opt_query] [ "Ltac2" "Eval" ltac2_expr(e) ] => { Vernacextend.classify_as_sideeff } -> {
+  fun ~pstate -> Tac2entries.perform_eval ~pstate e
   }
 END
 
@@ -899,15 +902,6 @@ END
 
 let _ = Pvernac.register_proof_mode "Ltac2" tac2mode
 
-}
-
-VERNAC ARGUMENT EXTEND ltac2_expr
-PRINTED BY { pr_ltac2expr }
-| [ tac2expr(e) ] -> { e }
-END
-
-{
-
 open G_ltac
 open Vernacextend
 
@@ -917,9 +911,7 @@ VERNAC { tac2mode } EXTEND VernacLtac2
 | ![proof] [ ltac2_expr(t) ltac_use_default(default) ] =>
     { classify_as_proofstep } -> {
 (*     let g = Option.default (Proof_global.get_default_goal_selector ()) g in *)
-  fun ~pstate ->
-    Option.map (fun pstate -> Tac2entries.call ~pstate ~default t) pstate
-  }
+  fun ~pstate -> Tac2entries.call ~pstate ~default t }
 END
 
 {
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index 254c2e5086..246fe47c4a 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -769,13 +769,12 @@ let perform_eval ~pstate e =
 
 (** Toplevel entries *)
 
-let register_struct ?local ~pstate str = match str with
+let register_struct ?local str = match str with
 | StrVal (mut, isrec, e) -> register_ltac ?local ~mut isrec e
 | StrTyp (isrec, t) -> register_type ?local isrec t
 | StrPrm (id, t, ml) -> register_primitive ?local id t ml
 | StrSyn (tok, lev, e) -> register_notation ?local tok lev e
 | StrMut (qid, e) -> register_redefinition ?local qid e
-| StrRun e -> perform_eval ~pstate e
 
 (** Toplevel exception *)
 
@@ -857,7 +856,7 @@ let print_ltac qid =
 (** Calling tactics *)
 
 let solve ~pstate default tac =
-  let pstate, status = Proof_global.with_current_proof begin fun etac p ->
+  let pstate, status = Proof_global.with_proof begin fun etac p ->
     let with_end_tac = if default then Some etac else None in
     let g = Goal_select.get_default_goal_selector () in
     let (p, status) = Pfedit.solve g None tac ?with_end_tac p in
diff --git a/user-contrib/Ltac2/tac2entries.mli b/user-contrib/Ltac2/tac2entries.mli
index e02c126e71..273cf02c9b 100644
--- a/user-contrib/Ltac2/tac2entries.mli
+++ b/user-contrib/Ltac2/tac2entries.mli
@@ -23,13 +23,14 @@ val register_primitive : ?local:bool ->
 
 val register_struct
   :  ?local:bool
-  -> pstate:Proof_global.pstate option
   -> strexpr
   -> unit
 
 val register_notation : ?local:bool -> sexpr list -> int option ->
   raw_tacexpr -> unit
 
+val perform_eval : pstate:Proof_global.pstate option -> raw_tacexpr -> unit
+
 (** {5 Notations} *)
 
 type scope_rule =
@@ -50,7 +51,7 @@ val print_ltac : Libnames.qualid -> unit
 (** {5 Eval loop} *)
 
 (** Evaluate a tactic expression in the current environment *)
-val call : pstate:Proof_global.t -> default:bool -> raw_tacexpr -> Proof_global.t
+val call : pstate:Proof_global.pstate -> default:bool -> raw_tacexpr -> Proof_global.pstate
 
 (** {5 Toplevel exceptions} *)
 
diff --git a/user-contrib/Ltac2/tac2expr.mli b/user-contrib/Ltac2/tac2expr.mli
index 2e7dfc42db..af7bc32785 100644
--- a/user-contrib/Ltac2/tac2expr.mli
+++ b/user-contrib/Ltac2/tac2expr.mli
@@ -168,8 +168,6 @@ type strexpr =
   (** Syntactic extensions *)
 | StrMut of qualid * raw_tacexpr
   (** Redefinition of mutable globals *)
-| StrRun of raw_tacexpr
-  (** Toplevel evaluation of an expression *)
 
 (** {5 Dynamic semantics} *)
 
diff --git a/vernac/classes.ml b/vernac/classes.ml
index c783531f91..b9f57c0727 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -404,7 +404,7 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps decl ids te
   | None ->
     pstate
 
-let do_instance ~pstate env env' sigma ?hook ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props =
+let do_instance env env' sigma ?hook ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props =
   let props =
     match props with
     | Some (true, { CAst.v = CRecord fs }) ->
@@ -487,17 +487,18 @@ let do_instance ~pstate env env' sigma ?hook ~tac ~global ~poly ~program_mode ct
     if not (Evd.has_undefined sigma) && not (Option.is_empty props) then
       let term = to_constr sigma (Option.get term) in
       (declare_instance_constant pri global imps ?hook id decl poly sigma term termtype;
-       pstate)
+       None)
     else if program_mode then
-      (declare_instance_program  env sigma ~global ~poly id pri imps decl term termtype ; pstate)
+      (declare_instance_program  env sigma ~global ~poly id pri imps decl term termtype;
+       None)
     else if Option.is_empty props then
-      let pstate' =
+      let pstate =
         Flags.silently (fun () ->
             declare_instance_open sigma ?hook ~tac ~global ~poly
               id pri imps decl (List.map RelDecl.get_name ctx) term termtype)
           ()
       in
-      Some (Proof_global.push ~ontop:pstate pstate')
+      Some pstate
     else CErrors.user_err Pp.(str "Unsolved obligations remaining.") in
   id, pstate
 
@@ -529,7 +530,7 @@ let interp_instance_context ~program_mode env ctx ?(generalize=false) pl tclass
   let sigma = resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:true env sigma in
   sigma, cl, u, c', ctx', ctx, imps, args, decl
 
-let new_instance ~pstate ?(global=false) ~program_mode
+let new_instance ?(global=false) ~program_mode
     poly instid ctx cl props
     ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri =
   let env = Global.env() in
@@ -545,7 +546,7 @@ let new_instance ~pstate ?(global=false) ~program_mode
       Namegen.next_global_ident_away i (Termops.vars_of_env env)
   in
   let env' = push_rel_context ctx env in
-  do_instance ~pstate env env' sigma ?hook ~tac ~global ~poly ~program_mode
+  do_instance env env' sigma ?hook ~tac ~global ~poly ~program_mode
     cty k u ctx ctx' pri decl imps subst id props
 
 let declare_new_instance ?(global=false) ~program_mode poly instid ctx cl pri =
diff --git a/vernac/classes.mli b/vernac/classes.mli
index f80dbb9897..d441fd342c 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -32,8 +32,7 @@ val existing_instance : bool -> qualid -> Hints.hint_info_expr option -> unit
 (** globality, reference, optional priority and pattern information *)
 
 val new_instance :
-  pstate:Proof_global.t option
-  -> ?global:bool (** Not global by default. *)
+  ?global:bool (** Not global by default. *)
   -> program_mode:bool
   -> Decl_kinds.polymorphic
   -> name_decl
@@ -44,7 +43,7 @@ val new_instance :
   -> ?tac:unit Proofview.tactic
   -> ?hook:(GlobRef.t -> unit)
   -> Hints.hint_info_expr
-  -> Id.t * Proof_global.t option (* May open a proof *)
+  -> Id.t * Proof_global.pstate option (* May open a proof *)
 
 val declare_new_instance
   : ?global:bool (** Not global by default. *)
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index f92c1f9c27..34b5e13cd8 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -60,6 +60,10 @@ let with_pstate ~pstate f =
   vernac_require_open_proof ~pstate
     (fun ~pstate -> f ~pstate:(Proof_global.get_current_pstate pstate))
 
+let modify_pstate ~pstate f =
+  vernac_require_open_proof ~pstate (fun ~pstate ->
+      Some (Proof_global.modify_current_pstate (fun pstate -> f ~pstate) pstate))
+
 let get_current_or_global_context ~pstate =
   match pstate with
   | None -> let env = Global.env () in Evd.(from_env env, env)
@@ -1100,7 +1104,7 @@ let focus_command_cond = Proof.no_cond command_focus
      all tactics fail if there are no further goals to prove. *)
 
 let vernac_solve_existential ~pstate n com =
-  Proof_global.simple_with_current_proof (fun _ p ->
+  Proof_global.modify_proof (fun p ->
       let intern env sigma = Constrintern.intern_constr env sigma com in
       Proof.V82.instantiate_evar (Global.env ()) n intern p) pstate
 
@@ -2441,7 +2445,8 @@ let rec interp_expr ?proof ~atts ~st c : Proof_global.t option =
 
   (* Type classes *)
   | VernacInstance (name, bl, t, props, info) ->
-    snd @@ with_def_attributes ~atts (vernac_instance ~pstate name bl t props info)
+    with_maybe_open_proof ~pstate (fun ~pstate:_ ->
+        snd @@ with_def_attributes ~atts (vernac_instance name bl t props info))
   | VernacDeclareInstance (id, bl, inst, info) ->
     with_def_attributes ~atts vernac_declare_instance id bl inst info;
     pstate
@@ -2459,7 +2464,7 @@ let rec interp_expr ?proof ~atts ~st c : Proof_global.t option =
   (* Solving *)
   | VernacSolveExistential (n,c) ->
     unsupported_attributes atts;
-    Some (vernac_require_open_proof ~pstate (vernac_solve_existential n c))
+    modify_pstate ~pstate (vernac_solve_existential n c)
 
   (* Auxiliary file and library management *)
   | VernacAddLoadPath (isrec,s,alias) ->
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 12451370c8..5e6e9fdb0f 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -44,6 +44,10 @@ val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr
 (** Helper *)
 val vernac_require_open_proof : pstate:Proof_global.t option -> (pstate:Proof_global.t -> 'a) -> 'a
 
+val with_pstate : pstate:Proof_global.t option -> (pstate:Proof_global.pstate -> 'a) -> 'a
+
+val modify_pstate : pstate:Proof_global.t option -> (pstate:Proof_global.pstate -> Proof_global.pstate) -> Proof_global.t option
+
 (* Flag set when the test-suite is called. Its only effect to display
    verbose information for `Fail` *)
 val test_mode : bool ref
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index 9ab2d00fc2..6eb618ad0a 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -34,6 +34,8 @@ type t = {
   shallow : bool                   (* is the state trimmed down (libstack) *)
 }
 
+let pstate st = Option.map Proof_global.get_current_pstate st.proof
+
 let s_cache = ref None
 let s_proof = ref None
 
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index dff81ad9bb..3d21b475e9 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -25,6 +25,8 @@ type t = {
   shallow : bool                   (* is the state trimmed down (libstack) *)
 }
 
+val pstate : t -> Proof_global.pstate option
+
 val freeze_interp_state : marshallable:bool -> t
 val unfreeze_interp_state : t -> unit