diff options
| -rw-r--r-- | proofs/goal.ml | 2 | ||||
| -rw-r--r-- | proofs/goal.mli | 2 | ||||
| -rw-r--r-- | proofs/proof.ml | 9 | ||||
| -rw-r--r-- | proofs/proof.mli | 3 | ||||
| -rw-r--r-- | stm/stm.ml | 19 | ||||
| -rw-r--r-- | stm/stm.mli | 3 |
6 files changed, 34 insertions, 4 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml index 1440d1636b..c14c0a8a77 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -143,3 +143,5 @@ module V82 = struct ) ~init:(concl sigma gl) env end + +module Set = Set.Make(struct type t = goal let compare = Evar.compare end) diff --git a/proofs/goal.mli b/proofs/goal.mli index b8c979ad7a..a033d6daab 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -71,3 +71,5 @@ module V82 : sig val abstract_type : Evd.evar_map -> goal -> EConstr.types end + +module Set : sig include Set.S with type elt = goal end diff --git a/proofs/proof.ml b/proofs/proof.ml index 0d355890c5..8bbd82bb0a 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -488,3 +488,12 @@ module V82 = struct { pr with proofview ; shelf } end + +let all_goals p = + let add gs set = + List.fold_left (fun s g -> Goal.Set.add g s) set gs in + let (goals,stack,shelf,given_up,_) = proof p in + let set = add goals Goal.Set.empty in + let set = List.fold_left (fun s gs -> let (g1, g2) = gs in add g1 (add g2 set)) set stack in + let set = add shelf set in + add given_up set diff --git a/proofs/proof.mli b/proofs/proof.mli index 33addf13d7..511dcc2e00 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -210,3 +210,6 @@ module V82 : sig (* Implements the Existential command *) val instantiate_evar : int -> Constrexpr.constr_expr -> t -> t end + +(* returns the set of all goals in the proof *) +val all_goals : t -> Goal.Set.t 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], |