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.

6 files changed, 26 insertions, 13 deletions

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