From 8abacf00c6c39ec98085d531737d18edc9c19b2a Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 2 May 2019 19:46:02 +0200
Subject: Proof_global: pass only 1 pstate when we don't want the proof stack

Typically instead of [start_proof : ontop:Proof_global.t option -> bla ->
Proof_global.t] we have [start_proof : bla -> Proof_global.pstate] and
the pstate is pushed on the stack by a caller around the
vernacentries/mlg level.

Naming can be a bit awkward, hopefully it can be improved (maybe in a
followup PR).

We can see some patterns appear waiting for nicer combinators, eg in
mlg we often only want to work with the current proof, not the stack.

Behaviour should be similar modulo bugs, let's see what CI says.
---
 doc/plugin_tutorial/tuto1/src/g_tuto1.mlg | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'doc/plugin_tutorial')

diff --git a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
index 75251d8e33..147b0df567 100644
--- a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
+++ b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
@@ -146,11 +146,12 @@ END
 
 VERNAC COMMAND EXTEND ExploreProof CLASSIFIED AS QUERY
 | ![ proof ] [ "Cmd9" ] ->
-  { fun ~pstate ->
-    Option.iter (fun (pstate : Proof_global.t) ->
+  { 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)) pstate;
-    pstate }
+          (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf)) ontop;
+    ontop }
 END
-- 
cgit v1.2.3


From b8842c3c8d6e6d9d4c19a75453fca9f94de6fa49 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 3 May 2019 14:14:40 +0200
Subject: 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.
---
 doc/plugin_tutorial/tuto1/src/g_tuto1.mlg | 16 +++++++---------
 1 file changed, 7 insertions(+), 9 deletions(-)

(limited to 'doc/plugin_tutorial')

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
-- 
cgit v1.2.3