diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-05-27 23:22:04 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-10-17 02:19:11 +0200 |
| commit | 19bbc3fd946555aa1fa1fc23d805a4eb3d13bc45 (patch) | |
| tree | 678afe57f554900aa0c737dc36f53a4c3ece1577 /stm/proofBlockDelimiter.ml | |
| parent | d9704f80a4f4b565f77368dbf7c9650d301a233d (diff) | |
[stm] Move interpretation state to Vernacentries
We still don't thread the state there, but this is a start of the
needed infrastructure.
Diffstat (limited to 'stm/proofBlockDelimiter.ml')
| -rw-r--r-- | stm/proofBlockDelimiter.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |