From a2549c7f716e870ea19fdbfd7b5493117fe21e76 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 9 Dec 2018 05:50:12 +0100
Subject: [proof] Rework proof interface.

- deprecate the old 5-tuple accessor in favor of a view record,

- move `name` and `kind` proof data from `Proof_global` to `Proof`,
  this will prove useful in subsequent functionalizations of the
  interface, in particular this is what abstract, which lives in the
  monads, needs in order no to access global state.

- Note that `Proof.t` and `Proof_global.t` are redundant anyways.
---
 stm/proofBlockDelimiter.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'stm/proofBlockDelimiter.ml')

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