diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 19 | ||||
| -rw-r--r-- | stm/stm.mli | 3 |
2 files changed, 18 insertions, 4 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 2e9bf71e49..635bf9bf31 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 (* }}} *) 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], |