From a828bcedb8ad60c5b1f4cf71f92f24f2c1197ecb Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Wed, 8 Aug 2018 18:45:47 -0700
Subject: Ensure_prev_proof returns a proof that has underlying differences
 from the specified version (i.e., skip over versions with proofview-only
 differences).

---
 proofs/goal.ml   | 2 ++
 proofs/goal.mli  | 2 ++
 proofs/proof.ml  | 9 +++++++++
 proofs/proof.mli | 3 +++
 4 files changed, 16 insertions(+)

(limited to 'proofs')

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
-- 
cgit v1.2.3


From 2dc65d41b0c3b3481958e1e224fd5ef05f57f243 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Tue, 7 Aug 2018 11:59:11 -0700
Subject: Current diff code only compares the first current goal of the old and
 new proof states.  That's not always correct.  This change will a) show diffs
 for all displayed goals and b) correctly match goals between the old and new
 proof states.

For example, "split." will show diffs for both resulting goals.
"all: swap 1 2" will show the same diffs as for the old proof state, though
in a different position in the output.

Please see comments before Proof_diffs.make_goal_map_i and Proof_diffs.match_goals
for a description of how goals are matched between old and new proofs.
---
 proofs/pfedit.ml  | 21 ++++++++++++---------
 proofs/pfedit.mli |  2 +-
 2 files changed, 13 insertions(+), 10 deletions(-)

(limited to 'proofs')

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index d971c28a26..e6507332b1 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -51,23 +51,22 @@ let _ = CErrors.register_handler begin function
   | _ -> raise CErrors.Unhandled
 end
 
-let get_nth_V82_goal i =
-  let p = Proof_global.give_me_the_proof () in
+let get_nth_V82_goal p i =
   let goals,_,_,_,sigma = Proof.proof p in
   try { it = List.nth goals (i-1) ; sigma }
   with Failure _ -> raise NoSuchGoal
 
-let get_goal_context_gen i =
-  let { it=goal ; sigma=sigma; } =  get_nth_V82_goal i in
+let get_goal_context_gen p i =
+  let { it=goal ; sigma=sigma; } = get_nth_V82_goal p i in
   (sigma, Refiner.pf_env { it=goal ; sigma=sigma; })
 
 let get_goal_context i =
-  try get_goal_context_gen i
+  try get_goal_context_gen (Proof_global.give_me_the_proof ()) i
   with Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof.")
      | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.")
 
 let get_current_goal_context () =
-  try get_goal_context_gen 1
+  try get_goal_context_gen (Proof_global.give_me_the_proof ()) 1
   with Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof.")
      | NoSuchGoal -> 
     (* spiwack: returning empty evar_map, since if there is no goal, under focus,
@@ -75,14 +74,18 @@ let get_current_goal_context () =
     let env = Global.env () in
     (Evd.from_env env, env)
 
-let get_current_context () =
-  try get_goal_context_gen 1
+let get_current_context ?p () =
+  let current_proof_by_default = function
+    | Some p -> p
+    | None -> Proof_global.give_me_the_proof ()
+  in
+  try get_goal_context_gen (current_proof_by_default p) 1
   with Proof_global.NoCurrentProof ->
     let env = Global.env () in
     (Evd.from_env env, env)
      | NoSuchGoal ->
         (* No more focused goals ? *)
-        let p = Proof_global.give_me_the_proof () in
+        let p = (current_proof_by_default p) in
         let evd = Proof.in_proof p (fun x -> x) in
         (evd, Global.env ())
 
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index e02b5ab956..5feb5bd645 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -60,7 +60,7 @@ val get_current_goal_context : unit -> Evd.evar_map * env
   If there is no pending proof then it returns the current global
   environment and empty evar_map. *)
 
-val get_current_context : unit -> Evd.evar_map * env
+val get_current_context : ?p:Proof.t -> unit -> Evd.evar_map * env
 
 (** [current_proof_statement] *)
 
-- 
cgit v1.2.3