Ensure_prev_proof returns a proof that has underlying differences from

the specified version (i.e., skip over versions with proofview-only differences).

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],