diff options
Diffstat (limited to 'stm/proofBlockDelimiter.ml')
| -rw-r--r-- | stm/proofBlockDelimiter.ml | 12 |
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 ] |