diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/proofBlockDelimiter.ml | 1 | ||||
| -rw-r--r-- | stm/stm.ml | 6 |
2 files changed, 5 insertions, 2 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 diff --git a/stm/stm.ml b/stm/stm.ml index b2bfa552b4..0efea0b8e0 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -881,7 +881,7 @@ end = struct (* {{{ *) let invalidate_cur_state () = cur_id := Stateid.dummy type proof_part = - Proof_global.t option * + Proof_global.stack option * int * (* Evarutil.meta_counter_summary_tag *) int * (* Evd.evar_counter_summary_tag *) Obligations.program_info Names.Id.Map.t (* Obligations.program_tcc_summary_tag *) @@ -1168,7 +1168,9 @@ end = struct (* {{{ *) let get_proof ~doc id = match state_of_id ~doc id with - | `Valid (Some vstate) -> Option.map Proof_global.give_me_the_proof vstate.Vernacstate.proof + | `Valid (Some vstate) -> + Option.map (fun p -> Proof_global.(give_me_the_proof (get_current_pstate p))) + vstate.Vernacstate.proof | _ -> None let undo_vernac_classifier v ~doc = |