Ensure_prev_proof returns a proof that has underlying differences from

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

1 files changed, 9 insertions, 0 deletions

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