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.

4 files changed, 18 insertions, 28 deletions

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