diff options
Diffstat (limited to 'stm/proofBlockDelimiter.ml')
| -rw-r--r-- | stm/proofBlockDelimiter.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml index 04f10e7399..dfa681395a 100644 --- a/stm/proofBlockDelimiter.ml +++ b/stm/proofBlockDelimiter.ml @@ -50,6 +50,7 @@ let is_focused_goal_simple ~doc id = | `Expired | `Error _ | `Valid None -> `Not | `Valid (Some { Vernacstate.proof }) -> Option.cata (fun proof -> + let proof = Proof_global.get_current_pstate proof in 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 |