From 19bbc3fd946555aa1fa1fc23d805a4eb3d13bc45 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Sat, 27 May 2017 23:22:04 +0200
Subject: [stm] Move interpretation state to Vernacentries

We still don't thread the state there, but this is a start of the
needed infrastructure.
---
 stm/proofBlockDelimiter.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'stm/proofBlockDelimiter.ml')

diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index b46556ea6..01b75e496 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -46,7 +46,7 @@ let simple_goal sigma g gs =
 let is_focused_goal_simple ~doc id =
   match state_of_id ~doc id with
   | `Expired | `Error _ | `Valid None -> `Not
-  | `Valid (Some { proof }) ->
+  | `Valid (Some { Vernacentries.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
-- 
cgit v1.2.3