diff options
Diffstat (limited to 'stm/proofBlockDelimiter.ml')
| -rw-r--r-- | stm/proofBlockDelimiter.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml index 230a3207a8..d13763cdec 100644 --- a/stm/proofBlockDelimiter.ml +++ b/stm/proofBlockDelimiter.ml @@ -49,12 +49,13 @@ 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 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 + Option.cata (fun proof -> + let proof = Proof_global.give_me_the_proof 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) `Not proof type 'a until = [ `Stop | `Found of static_block_declaration | `Cont of 'a ] |