diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 23 | ||||
| -rw-r--r-- | stm/stm.mli | 3 |
2 files changed, 20 insertions, 6 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 2e9bf71e49..b7ba163309 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1231,9 +1231,22 @@ end = struct (* {{{ *) let get_prev_proof ~doc id = try - let did = fold_until back_tactic 1 id in - get_proof ~doc did - with Not_found -> None + let np = get_proof ~doc id in + match np with + | None -> None + | Some cp -> + let did = ref id in + let rv = ref np in + let done_ = ref false in + while not !done_ do + did := fold_until back_tactic 1 !did; + rv := get_proof ~doc !did; + done_ := match !rv with + | Some rv -> not (Goal.Set.equal (Proof.all_goals rv) (Proof.all_goals cp)) + | None -> true + done; + !rv + with Not_found | Proof_global.NoCurrentProof -> None end (* }}} *) @@ -1996,7 +2009,7 @@ end = struct (* {{{ *) 1 goals in TaskQueue.join queue; let assign_tac : unit Proofview.tactic = - Proofview.(Goal.nf_enter begin fun g -> + Proofview.(Goal.enter begin fun g -> let gid = Goal.goal g in let f = try List.assoc gid res @@ -2288,7 +2301,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = | `Leaks -> Exninfo.iraise exn | `ValidBlock { base_state; goals_to_admit; recovery_command } -> begin let tac = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> if CList.mem_f Evar.equal (Proofview.Goal.goal gl) goals_to_admit then Proofview.give_up else Proofview.tclUNIT () diff --git a/stm/stm.mli b/stm/stm.mli index 7f70ea18da..1e5ceb7e23 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -111,7 +111,8 @@ val add : doc:doc -> ontop:Stateid.t -> ?newtip:Stateid.t -> doc * Stateid.t * [ `NewTip | `Unfocus of Stateid.t ] (* Returns the proof state before the last tactic that was applied at or before -the specified state. Used to compute proof diffs. *) +the specified state AND that has differences in the underlying proof (i.e., +ignoring proofview-only changes). Used to compute proof diffs. *) val get_prev_proof : doc:doc -> Stateid.t -> Proof.t option (* [query at ?report_with cmd] Executes [cmd] at a given state [at], |