Merge PR #9172: [proof] Rework proof interface.

1 files changed, 6 insertions, 6 deletions

diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index b8af2bcd56..230a3207a8 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -49,12 +49,12 @@ let is_focused_goal_simple ~doc id =
   match state_of_id ~doc id with
   | `Expired | `Error _ | `Valid None -> `Not
   | `Valid (Some { Vernacstate.proof }) ->
-       let proof = Proof_global.proof_of_state proof in
-       let focused, r1, r2, r3, sigma = Proof.proof proof in
-       let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ r2 @ r3 in
-       if List.for_all (fun x -> simple_goal sigma x rest) focused
-       then `Simple focused
-       else `Not
+    let proof = Proof_global.proof_of_state 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
+    if List.for_all (fun x -> simple_goal sigma x rest) focused
+    then `Simple focused
+    else `Not
 
 type 'a until = [ `Stop | `Found of static_block_declaration | `Cont of 'a ]