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, 3 insertions, 8 deletions

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