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.

1 files changed, 8 insertions, 3 deletions

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) ->