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.
---
 stm/proofBlockDelimiter.ml | 1 +
 stm/stm.ml                 | 4 +++-
 2 files changed, 4 insertions(+), 1 deletion(-)

(limited to 'stm')

diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index 04f10e7399..dfa681395a 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -50,6 +50,7 @@ let is_focused_goal_simple ~doc id =
   | `Expired | `Error _ | `Valid None -> `Not
   | `Valid (Some { Vernacstate.proof }) ->
     Option.cata (fun proof ->
+        let proof = Proof_global.get_current_pstate proof in
         let proof = Proof_global.give_me_the_proof proof in
         let Proof.{ goals=focused; stack=r1; shelf=r2; given_up=r3; sigma } = Proof.data proof in
         let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ r2 @ r3 in
diff --git a/stm/stm.ml b/stm/stm.ml
index b2bfa552b4..64f9e4aacf 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1168,7 +1168,9 @@ end = struct (* {{{ *)
 
   let get_proof ~doc id =
     match state_of_id ~doc id with
-    | `Valid (Some vstate) -> Option.map Proof_global.give_me_the_proof vstate.Vernacstate.proof
+    | `Valid (Some vstate) ->
+      Option.map (fun p -> Proof_global.(give_me_the_proof (get_current_pstate p)))
+        vstate.Vernacstate.proof
     | _ -> None
 
   let undo_vernac_classifier v ~doc =
-- 
cgit v1.2.3