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.

2 files changed, 13 insertions, 10 deletions

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] *)