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.

7 files changed, 480 insertions, 139 deletions

diff --git a/ide/idetop.ml b/ide/idetop.ml
index d846b3abb5..8a221a93e9 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -204,27 +204,35 @@ let export_pre_goals pgs =
     Interface.given_up_goals = pgs.Proof.given_up_goals
   }
 
-let add_diffs oldp newp intf =
-  let open Interface in
-  let (hyps_pp_list, concl_pp) = Proof_diffs.diff_first_goal oldp newp in
-  match intf.fg_goals with
-  | [] -> intf
-  | first_goal :: tl ->
-    { intf with fg_goals = { first_goal with goal_hyp = hyps_pp_list; goal_ccl = concl_pp } :: tl }
-
 let goals () =
   let doc = get_doc () in
   set_doc @@ Stm.finish ~doc;
   try
     let newp = Proof_global.give_me_the_proof () in
-    let intf = export_pre_goals (Proof.map_structured_proof newp process_goal) in
-    if Proof_diffs.show_diffs () then
+    if Proof_diffs.show_diffs () then begin
       let oldp = Stm.get_prev_proof ~doc (Stm.get_current_state ~doc) in
+      let diff_goal_map = Proof_diffs.make_goal_map oldp newp in
+      let map_goal_for_diff ng = (* todo: move to proof_diffs.ml *)
+        try Evar.Map.find ng diff_goal_map  with Not_found -> ng
+      in
+
+      let process_goal_diffs nsigma ng =
+        let open Evd in
+        let og = map_goal_for_diff ng in
+        let og_s = match oldp with
+        | Some oldp ->
+          let (_,_,_,_,osigma) = Proof.proof oldp in
+          Some { it = og; sigma = osigma }
+        | None -> None
+        in
+        let (hyps_pp_list, concl_pp) = Proof_diffs.diff_goal_ide og_s ng nsigma in
+        { Interface.goal_hyp = hyps_pp_list; Interface.goal_ccl = concl_pp; Interface.goal_id = Goal.uid ng }
+      in
       try
-        Some (add_diffs oldp (Some newp) intf)
-      with Pp_diff.Diff_Failure _ -> Some intf
-    else
-      Some intf
+        Some (export_pre_goals (Proof.map_structured_proof newp process_goal_diffs))
+      with Pp_diff.Diff_Failure _ -> Some (export_pre_goals (Proof.map_structured_proof newp process_goal))
+    end else
+      Some (export_pre_goals (Proof.map_structured_proof newp process_goal))
   with Proof_global.NoCurrentProof -> None;;
 
 let evars () =
diff --git a/printing/printer.ml b/printing/printer.ml
index 5b3ead181f..804999986c 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -494,17 +494,17 @@ let pr_transparent_state (ids, csts) =
 	str"CONSTANTS: " ++ pr_cpred csts ++ fnl ())
 
 (* display complete goal
- prev_gs has info on the previous proof step for diffs
- gs has info on the current proof step
+ og_s has goal+sigma on the previous proof step for diffs
+ g_s has goal+sigma on the current proof step
  *)
-let pr_goal ?(diffs=false) ?prev_gs gs =
-  let g = sig_it gs in
-  let sigma = project gs in
+let pr_goal ?(diffs=false) ?og_s g_s =
+  let g = sig_it g_s in
+  let sigma = project g_s in
   let env = Goal.V82.env sigma g in
   let concl = Goal.V82.concl sigma g in
   let goal =
     if diffs then
-      Proof_diffs.diff_goals ?prev_gs (Some gs)
+      Proof_diffs.diff_goal ?og_s g sigma
     else
       pr_context_of env sigma ++ cut () ++
         str "============================" ++ cut ()  ++
@@ -525,13 +525,18 @@ let pr_goal_name sigma g =
 let pr_goal_header nme sigma g =
   let (g,sigma) = Goal.V82.nf_evar sigma g in
   str "subgoal " ++ nme ++ (if should_tag() then pr_goal_tag g else str"")
-  ++ (if should_gname() then str " " ++ Pp.surround (pr_existential_key sigma g) else mt ())  
+  ++ (if should_gname() then str " " ++ Pp.surround (pr_existential_key sigma g) else mt ())
 
 (* display the conclusion of a goal *)
-let pr_concl n sigma g =
+let pr_concl n ?(diffs=false) ?og_s sigma g =
   let (g,sigma) = Goal.V82.nf_evar sigma g in
   let env = Goal.V82.env sigma g in
-  let pc = pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g) in
+  let pc =
+    if diffs then
+      Proof_diffs.diff_concl ?og_s sigma g
+    else
+      pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g)
+  in
   let header = pr_goal_header (int n) sigma g in
   header ++ str " is:" ++ cut () ++ str" "  ++ pc
 
@@ -698,13 +703,25 @@ let print_dependent_evars gl sigma seeds =
   in
   constraints ++ evars ()
 
+module GoalMap = Evar.Map
+
 (* Print open subgoals. Checks for uninstantiated existential variables *)
 (* spiwack: [seeds] is for printing dependent evars in emacs mode. *)
 (* spiwack: [pr_first] is true when the first goal must be singled out
    and printed in its entirety. *)
-(* [prev] is the previous proof step, used for diffs *)
-let pr_subgoals ?(pr_first=true) ?(diffs=false) ?prev
+(* [os_map] is derived from the previous proof step, used for diffs *)
+let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map
                         close_cmd sigma ~seeds ~shelf ~stack ~unfocused ~goals =
+  let diff_goal_map =
+    match os_map with
+    | Some (_, diff_goal_map) -> diff_goal_map
+    | None -> GoalMap.empty
+  in
+
+  let map_goal_for_diff ng = (* todo: move to proof_diffs.ml *)
+    try GoalMap.find ng diff_goal_map  with Not_found -> ng
+  in
+
   (** Printing functions for the extra informations. *)
   let rec print_stack a = function
     | [] -> Pp.int a
@@ -738,23 +755,23 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?prev
     else str" " (* non-breakable space *)
   in
 
+  let get_ogs g =
+    match os_map with
+    | Some (osigma, _) -> Some { it = map_goal_for_diff g; sigma = osigma }
+    | None -> None
+  in
   let rec pr_rec n = function
     | [] -> (mt ())
     | g::rest ->
-        let pc = pr_concl n sigma g in
+       let og_s = get_ogs g in
+       let pc = pr_concl n ~diffs ?og_s sigma g in
         let prest = pr_rec (n+1) rest in
         (cut () ++ pc ++ prest)
   in
   let print_multiple_goals g l =
     if pr_first then
-      let prev_gs =
-        match prev with
-        | Some (prev_goals, prev_sigma) ->
-          if prev_goals = [] then None
-          else Some { it = List.hd prev_goals; sigma = prev_sigma}
-        | None -> None
-      in
-      pr_goal ~diffs ?prev_gs { it = g ; sigma = sigma }
+      let og_s = get_ogs g in
+      pr_goal ~diffs ?og_s { it = g ; sigma = sigma }
       ++ (if l=[] then mt () else cut ())
       ++ pr_rec 2 l
     else 
@@ -797,7 +814,7 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?prev
 	++ print_dependent_evars (Some g1) sigma seeds
       )
 
-let pr_open_subgoals_diff ?(quiet=false) ?(diffs=false) ?prev_proof proof =
+let pr_open_subgoals_diff ?(quiet=false) ?(diffs=false) ?oproof proof =
   (* spiwack: it shouldn't be the job of the printer to look up stuff
      in the [evar_map], I did stuff that way because it was more
      straightforward, but seriously, [Proof.proof] should return
@@ -833,15 +850,15 @@ let pr_open_subgoals_diff ?(quiet=false) ?(diffs=false) ?prev_proof proof =
      let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in
      let bgoals_focused, bgoals_unfocused = List.partition (fun x -> List.mem x goals) bgoals in
      let unfocused_if_needed = if should_unfoc() then bgoals_unfocused else [] in
-     let prev = match prev_proof with
-       | Some op ->
-         let (ogoals , _, _, _, _) = Proof.proof op in
-         let { Evd.it = obgoals; sigma = osigma } = Proof.V82.background_subgoals op in
-         let obgoals_focused = List.filter (fun x -> List.mem x ogoals) obgoals in
-         Some (obgoals_focused, osigma)
-       | None -> None
+     let os_map = match oproof with
+       | Some op when diffs ->
+         let (_,_,_,_, osigma) = Proof.proof op in
+         let diff_goal_map = Proof_diffs.make_goal_map oproof proof in
+         Some (osigma, diff_goal_map)
+       | _ -> None
      in
-     pr_subgoals ~pr_first:true ~diffs ?prev None bsigma ~seeds ~shelf ~stack:[] ~unfocused:unfocused_if_needed ~goals:bgoals_focused
+     pr_subgoals ~pr_first:true ~diffs ?os_map None bsigma ~seeds ~shelf ~stack:[]
+        ~unfocused:unfocused_if_needed ~goals:bgoals_focused
   end
 
 let pr_open_subgoals ~proof =
@@ -1023,22 +1040,14 @@ let print_and_diff oldp newp =
   | Some proof ->
     let output =
       if Proof_diffs.show_diffs () then
-        try pr_open_subgoals_diff ~diffs:true ?prev_proof:oldp proof
+        try pr_open_subgoals_diff ~diffs:true ?oproof:oldp proof
         with Pp_diff.Diff_Failure msg -> begin
           (* todo: print the unparsable string (if we know it) *)
-          Feedback.msg_warning Pp.(str ("Diff failure:" ^ msg ^ "; showing results without diff highlighting" ));
+          Feedback.msg_warning Pp.(str ("Diff failure: " ^ msg) ++ cut()
+              ++ str "Showing results without diff highlighting" );
           pr_open_subgoals ~proof
         end
       else
         pr_open_subgoals ~proof
     in
     Feedback.msg_notice output;;
-
-(* Do diffs on the first goal returning a Pp. *)
-let diff_pr_open_subgoals ?(quiet=false) o_proof n_proof =
-  match n_proof with
-  | None -> Pp.mt ()
-  | Some proof ->
-    try pr_open_subgoals_diff ~quiet ~diffs:true ?prev_proof:o_proof proof
-    with Pp_diff.Diff_Failure _ -> pr_open_subgoals ~proof
-      (* todo: print the unparsable string (if we know it) *)
diff --git a/printing/printer.mli b/printing/printer.mli
index 971241d5f9..47be8b7eaa 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -171,26 +171,46 @@ val pr_transparent_state   : transparent_state -> Pp.t
 
 (** Proofs, these functions obey [Hyps Limit] and [Compact contexts]. *)
 
-val pr_goal                : ?diffs:bool -> ?prev_gs:(goal sigma) -> goal sigma -> Pp.t
-
-(** [pr_subgoals ~pr_first ~prev_proof pp sigma seeds shelf focus_stack unfocused goals]
-   prints the goals of the list [goals] followed by the goals in
-   [unfocused], in a short way (typically only the conclusion) except
-   for the first goal if [pr_first] is true. Also, if [diffs] is true
-   and [pr_first] is true, then highlight diffs relative to [prev] in the
-   output for first goal. This function prints only the
-   focused goals unless the conrresponding option
-   [enable_unfocused_goal_printing] is set. [seeds] is for printing
-   dependent evars (mainly for emacs proof tree mode). *)
-val pr_subgoals            : ?pr_first:bool -> ?diffs:bool -> ?prev:(goal list * evar_map) -> Pp.t option -> evar_map
+(** [pr_goal ~diffs ~og_s g_s] prints the goal specified by [g_s].  If [diffs] is true,
+    highlight the differences between the old goal, [og_s], and [g_s].  [g_s] and [og_s] are
+    records containing the goal and sigma for, respectively, the new and old proof steps,
+    e.g. [{ it = g ; sigma = sigma }].
+*)
+val pr_goal                : ?diffs:bool -> ?og_s:(goal sigma) -> goal sigma -> Pp.t
+
+(** [pr_subgoals ~pr_first ~diffs ~os_map close_cmd sigma ~seeds ~shelf ~stack ~unfocused ~goals]
+   prints the goals in [goals] followed by the goals in [unfocused] in a compact form
+   (typically only the conclusion).  If [pr_first] is true, print the first goal in full.
+   [close_cmd] is printed afterwards verbatim.
+
+   If [diffs] is true, then highlight diffs relative to [os_map] in the output for first goal.
+   [os_map] contains sigma for the old proof step and the goal map created by
+   [Proof_diffs.make_goal_map].
+
+   This function prints only the focused goals unless the corresponding option [enable_unfocused_goal_printing] is set.
+   [seeds] is for printing dependent evars (mainly for emacs proof tree mode).  [shelf] is from
+   Proof.proof and is used to identify shelved goals in a message if there are no more subgoals but
+   there are non-instantiated existential variables.  [stack] is used to print summary info on unfocused
+   goals.
+*)
+val pr_subgoals            : ?pr_first:bool -> ?diffs:bool -> ?os_map:(evar_map * Evar.t Evar.Map.t) -> Pp.t option -> evar_map
                              -> seeds:goal list -> shelf:goal list -> stack:int list
                              -> unfocused: goal list -> goals:goal list -> Pp.t
 
 val pr_subgoal             : int -> evar_map -> goal list -> Pp.t
-val pr_concl               : int -> evar_map -> goal -> Pp.t
 
-val pr_open_subgoals_diff  : ?quiet:bool -> ?diffs:bool -> ?prev_proof:Proof.t -> Proof.t -> Pp.t
-val diff_pr_open_subgoals  : ?quiet:bool -> Proof.t option -> Proof.t option -> Pp.t
+(** [pr_concl n ~diffs ~og_s sigma g] prints the conclusion of the goal [g] using [sigma].  The output
+    is labelled "subgoal [n]".  If [diffs] is true, highlight the differences between the old conclusion,
+    [og_s], and [g]+[sigma].  [og_s] is a record containing the old goal and sigma, e.g. [{ it = g ; sigma = sigma }].
+*)
+val pr_concl               : int -> ?diffs:bool -> ?og_s:(goal sigma) -> evar_map -> goal -> Pp.t
+
+(** [pr_open_subgoals_diff ~quiet ~diffs ~oproof proof] shows the context for [proof] as used by, for example, coqtop.
+    The first active goal is printed with all its antecedents and the conclusion.  The other active goals only show their
+     conclusions.  If [diffs] is true, highlight the differences between the old proof, [oproof], and [proof].  [quiet]
+     disables printing messages as Feedback.
+*)
+val pr_open_subgoals_diff  : ?quiet:bool -> ?diffs:bool -> ?oproof:Proof.t -> Proof.t -> Pp.t
 val pr_open_subgoals       : proof:Proof.t -> Pp.t
 val pr_nth_open_subgoal    : proof:Proof.t -> int -> Pp.t
 val pr_evar                : evar_map -> (Evar.t * evar_info) -> Pp.t
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index 3a81e908a7..5bb1053645 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -14,39 +14,26 @@ Proof General requires minor changes to make the diffs visible, but this code
 shouldn't break the existing version of PG.  See pp_diff.ml for details on how
 the diff works.
 
-Diffs are computed for the hypotheses and conclusion of the first goal between
-the old and new proofs.
+Diffs are computed for the hypotheses and conclusion of each goal in the new
+proof with its matching goal in the old proof.
 
-Diffs can be enabled with the Coq commmand "Set Diffs on|off|removed." or
-'-diffs "on"|"off"|"removed"' on the OS command line.  The "on" option shows only the
-new item with added text, while "removed" shows each modified item twice--once
-with the old value showing removed text and once with the new value showing
-added text.
+Diffs can be enabled in coqtop with 'Set Diffs "on"|"off"|"removed"' or
+'-diffs on|off|removed' on the OS command line.  In CoqIDE, they can be enabled
+from the View menu.  The "on" option shows only the new item with added text,
+while "removed" shows each modified item twice--once with the old value showing
+removed text and once with the new value showing added text.
 
 In CoqIDE, colors and highlights can be set in the Edit/Preferences/Tags panel.
 For coqtop, these can be set through the COQ_COLORS environment variable.
 
 Limitations/Possible enhancements:
 
-- If you go back to a prior proof step, diffs are not shown on the new current
-step.  Diffs will be shown again once you do another proof step.
-
-- Diffs are done between the first active goal in the old and new proofs.
-If, for example, the proof step completed a goal, then the new goal is a
-different goal, not a transformation of the old goal, so a diff is probably
-not appropriate.  (There's currently no way to tell when this happens or to
-accurately match goals across old and new proofs.
-See https://github.com/coq/coq/issues/7653)  This is also why only the
-first goal is diffed.
-
-- "Set Diffs "xx"." should reprint the current goal using the new option.
-
 - coqtop colors were chosen for white text on a black background.  They're
 not the greatest.  I didn't want to change the existing green highlight.
 Suggestions welcome.
 
 - coqtop underlines removed text because (per Wikipedia) the ANSI escape code
-for strikeout is not commonly supported (it didn't work on mine).  CoqIDE
+for strikeout is not commonly supported (it didn't work on my system).  CoqIDE
 uses strikeout on removed text.
 *)
 
@@ -54,8 +41,6 @@ open Pp_diff
 
 let diff_option = ref `OFF
 
-(* todo: Is there a way to persist the setting between sessions?
-   Eg if the user wants this as a permanent config setting? *)
 let read_diffs_option () = match !diff_option with
 | `OFF -> "off"
 | `ON -> "on"
@@ -136,7 +121,8 @@ let diff_hyps o_line_idents o_map n_line_idents n_map =
     (* use the order from the old line in case it's changed in the new *)
     let old_ids = if old_ids_uo = [] then [] else
       let orig = (StringMap.find (List.hd old_ids_uo) o_map).idents in
-      List.concat (List.map (contains orig) old_ids_uo) in
+      List.concat (List.map (contains orig) old_ids_uo)
+    in
 
     let setup ids map = if ids = [] then ("", Pp.mt ()) else
       let open Pp in
@@ -233,6 +219,12 @@ let to_tuple : Constr.compacted_declaration -> (Names.Id.t list * 'pc option * '
 
 (* XXX: Very unfortunately we cannot use the Proofview interface as
    Proof is still using the "legacy" one. *)
+let process_goal_concl sigma g : Constr.t * Environ.env =
+  let env  = Goal.V82.env   sigma g in
+  let ty   = Goal.V82.concl sigma g in
+  let ty   = EConstr.to_constr sigma ty in
+  (ty, env)
+
 let process_goal sigma g : Constr.t reified_goal =
   let env  = Goal.V82.env   sigma g in
   let hyps = Goal.V82.hyps  sigma g in
@@ -256,14 +248,29 @@ let pr_leconstr_core goal_concl_style env sigma t =
 
 let pr_lconstr_env env sigma c = pr_leconstr_core false env sigma (EConstr.of_constr c)
 
+let diff_concl ?og_s nsigma ng =
+  let open Evd in
+  let o_concl_pp = match og_s with
+    | Some { it=og; sigma=osigma } ->
+      let (oty, oenv) = process_goal_concl osigma og in
+      pp_of_type oenv osigma oty
+    | None -> Pp.mt()
+  in
+  let (nty, nenv) = process_goal_concl nsigma ng in
+  let n_concl_pp = pp_of_type nenv nsigma nty in
+
+  let show_removed = Some (show_removed ()) in
+
+  diff_pp_combined ~tokenize_string ?show_removed o_concl_pp n_concl_pp
+
 (* fetch info from a goal, returning (idents, map, concl_pp) where
-idents is a list with one entry for each hypothesis, each entry is the list of
-idents on the lhs of the hypothesis.  map is a map from ident to hyp_info
-reoords.  For example: for the hypotheses:
+idents is a list with one entry for each hypothesis, in which each entry
+is the list of idents on the lhs of the hypothesis.  map is a map from
+ident to hyp_info reoords.  For example: for the hypotheses:
   b : bool
   n, m : nat
 
-list will be [ ["b"]; ["n"; "m"] ]
+idents will be [ ["b"]; ["n"; "m"] ]
 
 map will contain:
   "b" -> { ["b"], Pp.t for ": bool"; false }
@@ -317,31 +324,314 @@ let hyp_list_to_pp hyps =
   | h :: tl -> List.fold_left (fun x y -> x ++ cut () ++ y) h tl
   | [] -> mt ();;
 
-(* Special purpuse, use only for the IDE interface,  *)
-let diff_first_goal o_proof n_proof =
-  let first_goal_info proof =
-    match proof with
-    | None -> ([], StringMap.empty, Pp.mt ())
-    | Some proof2 ->
-      let (goals,_,_,_,sigma) = Proof.proof proof2 in
-      match goals with
-      | hd :: tl -> goal_info hd sigma;
-      | _ -> ([], StringMap.empty, Pp.mt ())
-  in
-  diff_goal_info (first_goal_info o_proof) (first_goal_info n_proof);;
-
-let diff_goals ?prev_gs n_gs =
-  let unwrap gs =
-    match gs with
-    | Some gs ->
-      let goal = Evd.sig_it gs in
-      let sigma = Refiner.project gs in
-      goal_info goal sigma
-    | None -> ([], StringMap.empty, Pp.mt ())
-  in
-  let (hyps_pp_list, concl_pp) = diff_goal_info (unwrap prev_gs) (unwrap n_gs) in
+let unwrap g_s =
+  match g_s with
+  | Some g_s ->
+    let goal = Evd.sig_it g_s in
+    let sigma = Refiner.project g_s in
+    goal_info goal sigma
+  | None -> ([], StringMap.empty, Pp.mt ())
+
+let diff_goal_ide og_s ng nsigma =
+  diff_goal_info (unwrap og_s) (goal_info ng nsigma)
+
+let diff_goal ?og_s ng ns =
+  let (hyps_pp_list, concl_pp) = diff_goal_info (unwrap og_s) (goal_info ng ns) in
   let open Pp in
   v 0 (
     (hyp_list_to_pp hyps_pp_list) ++ cut () ++
     str "============================" ++ cut () ++
     concl_pp);;
+
+
+(*** Code to determine which calls to compare between the old and new proofs ***)
+
+open Constrexpr
+open Glob_term
+open Names
+open CAst
+
+(* Compare the old and new proof trees to identify the correspondence between
+new and old goals.  Returns a map from the new evar name to the old,
+e.g. "Goal2" -> "Goal1".  Assumes that proof steps only rewrite CEvar nodes
+and that CEvar nodes cannot contain other CEvar nodes.
+
+The comparison works this way:
+1. Traverse the old and new trees together (ogname = "", ot != nt):
+- if the old and new trees both have CEvar nodes, add an entry to the map from
+  the new evar name to the old evar name.  (Position of goals is preserved but
+  evar names may not be--see below.)
+- if the old tree has a CEvar node and the new tree has a different type of node,
+  we've found a changed goal.  Set ogname to the evar name of the old goal and
+  go to step 2.
+- any other mismatch violates the assumptions, raise an exception
+2. Traverse the new tree from the point of the difference (ogname <> "", ot = nt).
+- if the node is a CEvar, generate a map entry from the new evar name to ogname.
+
+Goal ids for unchanged goals appear to be preserved across proof steps.
+However, the evar name associated with a goal id may change in a proof step
+even if that goal is not changed by the tactic.  You can see this by enabling
+the call to db_goal_map and entering the following:
+
+  Parameter P : nat -> Prop.
+  Goal (P 1 /\ P 2 /\ P 3) /\ P 4.
+  split.
+  Show Proof.
+  split.
+  Show Proof.
+
+  Which gives you this summarized output:
+
+  > split.
+  New Goals: 3 -> Goal  4 -> Goal0              <--- goal 4 is "Goal0"
+  Old Goals: 1 -> Goal
+  Goal map: 3 -> 1  4 -> 1
+  > Show Proof.
+  (conj ?Goal ?Goal0)                           <--- goal 4 is the rightmost goal in the proof
+  > split.
+  New Goals: 6 -> Goal0  7 -> Goal1  4 -> Goal  <--- goal 4 is now "Goal"
+  Old Goals: 3 -> Goal  4 -> Goal0
+  Goal map: 6 -> 3  7 -> 3
+  > Show Proof.
+  (conj (conj ?Goal0 ?Goal1) ?Goal)             <--- goal 4 is still the rightmost goal in the proof
+ *)
+let match_goals ot nt =
+  let nevar_to_oevar = ref StringMap.empty in
+  (* ogname is "" when there is no difference on the current path.
+     It's set to the old goal's evar name once a rewitten goal is found,
+     at which point the code only searches for the replacing goals
+     (and ot is set to nt). *)
+  let rec match_goals_r ogname ot nt =
+    let constr_expr ogname exp exp2 =
+      match_goals_r ogname exp.v exp2.v
+    in
+    let constr_expr_opt ogname exp exp2 =
+      match exp, exp2 with
+      | Some expa, Some expb -> constr_expr ogname expa expb
+      | None, None -> ()
+      | _, _ -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (1)")
+    in
+    let local_binder_expr ogname exp exp2 =
+      match exp, exp2 with
+      | CLocalAssum (nal,bk,ty), CLocalAssum(nal2,bk2,ty2) ->
+        constr_expr ogname ty ty2
+      | CLocalDef (n,c,t), CLocalDef (n2,c2,t2) ->
+        constr_expr ogname c c2;
+        constr_expr_opt ogname t t2
+      | CLocalPattern p, CLocalPattern p2 ->
+        let (p,ty), (p2,ty2) = p.v,p2.v in
+        constr_expr_opt ogname ty ty2
+      | _, _ -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (2)")
+    in
+    let recursion_order_expr ogname exp exp2 =
+      match exp, exp2 with
+      | CStructRec, CStructRec -> ()
+      | CWfRec c, CWfRec c2 ->
+        constr_expr ogname c c2
+      | CMeasureRec (m,r), CMeasureRec (m2,r2) ->
+        constr_expr ogname m m2;
+        constr_expr_opt ogname r r2
+      | _, _ -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (3)")
+    in
+    let fix_expr ogname exp exp2 =
+      let (l,(lo,ro),lb,ce1,ce2), (l2,(lo2,ro2),lb2,ce12,ce22) = exp,exp2 in
+        recursion_order_expr ogname ro ro2;
+        List.iter2 (local_binder_expr ogname) lb lb2;
+        constr_expr ogname ce1 ce12;
+        constr_expr ogname ce2 ce22
+    in
+    let cofix_expr ogname exp exp2 =
+      let (l,lb,ce1,ce2), (l2,lb2,ce12,ce22) = exp,exp2 in
+        List.iter2 (local_binder_expr ogname) lb lb2;
+        constr_expr ogname ce1 ce12;
+        constr_expr ogname ce2 ce22
+    in
+    let case_expr ogname exp exp2 =
+      let (ce,l,cp), (ce2,l2,cp2) = exp,exp2 in
+      constr_expr ogname ce ce2
+    in
+    let branch_expr ogname exp exp2 =
+      let (cpe,ce), (cpe2,ce2) = exp.v,exp2.v in
+        constr_expr ogname ce ce2
+    in
+    let constr_notation_substitution ogname exp exp2 =
+      let (ce, cel, cp, lb), (ce2, cel2, cp2, lb2) = exp, exp2 in
+      List.iter2 (constr_expr ogname) ce ce2;
+      List.iter2 (fun a a2 -> List.iter2 (constr_expr ogname) a a2) cel cel2;
+      List.iter2 (fun a a2 -> List.iter2 (local_binder_expr ogname) a a2) lb lb2
+    in
+    begin
+    match ot, nt with
+    | CRef (ref,us), CRef (ref2,us2) -> ()
+    | CFix (id,fl), CFix (id2,fl2) ->
+      List.iter2 (fix_expr ogname) fl fl2
+    | CCoFix (id,cfl), CCoFix (id2,cfl2) ->
+      List.iter2 (cofix_expr ogname) cfl cfl2
+    | CProdN (bl,c2), CProdN (bl2,c22)
+    | CLambdaN (bl,c2), CLambdaN (bl2,c22) ->
+      List.iter2 (local_binder_expr ogname) bl bl2;
+      constr_expr ogname c2 c22
+    | CLetIn (na,c1,t,c2), CLetIn (na2,c12,t2,c22) ->
+      constr_expr ogname c1 c12;
+      constr_expr_opt ogname t t2;
+      constr_expr ogname c2 c22
+    | CAppExpl ((isproj,ref,us),args), CAppExpl ((isproj2,ref2,us2),args2) ->
+      List.iter2 (constr_expr ogname) args args2
+    | CApp ((isproj,f),args), CApp ((isproj2,f2),args2) ->
+      constr_expr ogname f f2;
+      List.iter2 (fun a a2 -> let (c, _) = a and (c2, _) = a2 in
+          constr_expr ogname c c2) args args2
+    | CRecord fs, CRecord fs2 ->
+      List.iter2 (fun a a2 -> let (_, c) = a and (_, c2) = a2 in
+          constr_expr ogname c c2) fs fs2
+    | CCases (sty,rtnpo,tms,eqns), CCases (sty2,rtnpo2,tms2,eqns2) ->
+        constr_expr_opt ogname rtnpo rtnpo2;
+        List.iter2 (case_expr ogname) tms tms2;
+        List.iter2 (branch_expr ogname) eqns eqns2
+    | CLetTuple (nal,(na,po),b,c), CLetTuple (nal2,(na2,po2),b2,c2) ->
+      constr_expr_opt ogname po po2;
+      constr_expr ogname b b2;
+      constr_expr ogname c c2
+    | CIf (c,(na,po),b1,b2), CIf (c2,(na2,po2),b12,b22) ->
+      constr_expr ogname c c2;
+      constr_expr_opt ogname po po2;
+      constr_expr ogname b1 b12;
+      constr_expr ogname b2 b22
+    | CHole (k,naming,solve), CHole (k2,naming2,solve2) -> ()
+    | CPatVar _, CPatVar _ -> ()
+    | CEvar (n,l), CEvar (n2,l2) ->
+      let oevar = if ogname = "" then Id.to_string n else ogname in
+      nevar_to_oevar := StringMap.add (Id.to_string n2) oevar !nevar_to_oevar;
+      List.iter2  (fun x x2 -> let (_, g) = x and (_, g2) = x2 in constr_expr ogname g g2)  l l2
+    | CEvar (n,l), nt' ->
+      (* pass down the old goal evar name *)
+      match_goals_r (Id.to_string n) nt' nt'
+    | CSort s, CSort s2 -> ()
+    | CCast (c,c'), CCast (c2,c'2) ->
+      constr_expr ogname c c2;
+      (match c', c'2 with
+      | CastConv a, CastConv a2
+      | CastVM a, CastVM a2
+      | CastNative a, CastNative a2 ->
+        constr_expr ogname a a2
+      | CastCoerce, CastCoerce -> ()
+      | _, _ -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (4)"))
+    | CNotation (ntn,args), CNotation (ntn2,args2) ->
+      constr_notation_substitution ogname args args2
+    | CGeneralization (b,a,c), CGeneralization (b2,a2,c2) ->
+      constr_expr ogname c c2
+    | CPrim p, CPrim p2 -> ()
+    | CDelimiters (key,e), CDelimiters (key2,e2) ->
+      constr_expr ogname e e2
+    | CProj (pr,c), CProj (pr2,c2) ->
+      constr_expr ogname c c2
+    | _, _ -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (5)")
+    end
+  in
+
+  (match ot with
+  | Some ot -> match_goals_r "" ot nt
+  | None -> ());
+  !nevar_to_oevar
+
+
+let to_constr p =
+  let open CAst in
+  let pprf = Proof.partial_proof p in
+  (* pprf generally has only one element, but it may have more in the derive plugin *)
+  let t = List.hd pprf in
+  let sigma, env = Pfedit.get_current_context ~p () in
+  let x = Constrextern.extern_constr false env sigma t in  (* todo: right options?? *)
+  x.v
+
+
+module GoalMap = Evar.Map
+
+let goal_to_evar g sigma = Id.to_string (Termops.pr_evar_suggested_name g sigma)
+
+[@@@ocaml.warning "-32"]
+let db_goal_map op np ng_to_og =
+  Printf.printf "New Goals: ";
+  let (ngoals,_,_,_,nsigma) = Proof.proof np in
+  List.iter (fun ng -> Printf.printf "%d -> %s  " (Evar.repr ng) (goal_to_evar ng nsigma)) ngoals;
+  (match op with
+  | Some op ->
+    let (ogoals,_,_,_,osigma) = Proof.proof op in
+    Printf.printf "\nOld Goals: ";
+    List.iter (fun og -> Printf.printf "%d -> %s  " (Evar.repr og) (goal_to_evar og osigma)) ogoals
+  | None -> ());
+  Printf.printf "\nGoal map: ";
+  GoalMap.iter (fun og ng -> Printf.printf "%d -> %d  " (Evar.repr og) (Evar.repr ng)) ng_to_og;
+  Printf.printf "\n"
+[@@@ocaml.warning "+32"]
+
+(* Create a map from new goals to old goals for proof diff.  The map only
+ has entries for new goals that are not the same as the corresponding old
+ goal; there are no entries for unchanged goals.
+
+ It proceeds as follows:
+ 1. Find the goal ids that were removed from the old proof and that were
+ added in the new proof.  If the same goal id is present in both proofs
+ then conclude the goal is unchanged (assumption).
+
+ 2. The code assumes that proof changes only take the form of replacing
+ one or more goal symbols (CEvars) with new terms.  Therefore:
+ - if there are no removals, the proofs are the same.
+ - if there are removals but no additions, then there are no new goals
+   that aren't the same as their associated old goals.  For the both of
+   these cases, the map is empty because there are no new goals that differ
+   from their old goals
+ - if there is only one removal, then any added goals should be mapped to
+   the removed goal.
+ - if there are more than 2 removals and more than one addition, call
+   match_goals to get a map between old and new evar names, then use this
+   to create the map from new goal ids to old goal ids for the differing goals.
+*)
+let make_goal_map_i op np =
+  let ng_to_og = ref GoalMap.empty in
+  match op with
+  | None -> !ng_to_og
+  | Some op ->
+    let open Goal.Set in
+    let ogs = Proof.all_goals op in
+    let ngs = Proof.all_goals np in
+    let rem_gs = diff ogs ngs in
+    let num_rems = cardinal rem_gs in
+    let add_gs = diff ngs ogs in
+    let num_adds = cardinal add_gs in
+
+    if num_rems = 0 then
+      !ng_to_og (* proofs are the same *)
+    else if num_adds = 0 then
+      !ng_to_og (* only removals *)
+    else if num_rems = 1 then begin
+      (* only 1 removal, some additions *)
+      let removed_g = List.hd (elements rem_gs) in
+      Goal.Set.iter (fun x -> ng_to_og := GoalMap.add x removed_g !ng_to_og) add_gs;
+      !ng_to_og
+    end else begin
+      (* >= 2 removals, >= 1 addition, need to match *)
+      let nevar_to_oevar = match_goals (Some (to_constr op)) (to_constr np) in
+
+      let oevar_to_og = ref StringMap.empty in
+      let (_,_,_,_,osigma) = Proof.proof op in
+      List.iter (fun og -> oevar_to_og := StringMap.add (goal_to_evar og osigma) og !oevar_to_og)
+          (Goal.Set.elements rem_gs);
+
+      try
+        let (_,_,_,_,nsigma) = Proof.proof np in
+        let get_og ng =
+          let nevar = goal_to_evar ng nsigma in
+          let oevar = StringMap.find nevar nevar_to_oevar in
+          let og = StringMap.find oevar !oevar_to_og in
+          og
+        in
+        Goal.Set.iter (fun ng -> ng_to_og := GoalMap.add ng (get_og ng) !ng_to_og) add_gs;
+        !ng_to_og
+      with Not_found -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (6)")
+    end
+
+let make_goal_map op np =
+  let ng_to_og = make_goal_map_i op np in
+  (*db_goal_map op np ng_to_og;*)
+  ng_to_og
diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli
index 482f03b686..832393e15f 100644
--- a/printing/proof_diffs.mli
+++ b/printing/proof_diffs.mli
@@ -15,8 +15,13 @@ val write_diffs_option : string -> unit
 (** Returns true if the diffs option is "on" or "removed" *)
 val show_diffs : unit -> bool
 
-(** Computes the diff between the first goal of two Proofs and returns
-the highlighted hypotheses and conclusion.
+open Evd
+open Proof_type
+open Environ
+open Constr
+
+(** Computes the diff between the goals of two Proofs and returns
+the highlighted lists of hypotheses and conclusions.
 
 If the strings used to display the goal are not lexable (this is believed
 unlikely), this routine will generate a Diff_Failure.  This routine may also
@@ -26,12 +31,7 @@ If you want to make your call especially bulletproof, catch these
 exceptions, print a user-visible message, then recall this routine with
 the first argument set to None, which will skip the diff.
 *)
-val diff_first_goal : Proof.t option -> Proof.t option -> Pp.t list * Pp.t
-
-open Evd
-open Proof_type
-open Environ
-open Constr
+val diff_goal_ide : goal sigma option -> goal -> Evd.evar_map -> Pp.t list * Pp.t
 
 (** Computes the diff between two goals
 
@@ -43,7 +43,7 @@ If you want to make your call especially bulletproof, catch these
 exceptions, print a user-visible message, then recall this routine with
 the first argument set to None, which will skip the diff.
 *)
-val diff_goals : ?prev_gs:(goal sigma) -> goal sigma option -> Pp.t
+val diff_goal : ?og_s:(goal sigma) -> goal -> Evd.evar_map -> Pp.t
 
 (** Convert a string to a list of token strings using the lexer *)
 val tokenize_string : string -> string list
@@ -52,6 +52,17 @@ val pr_letype_core         : bool -> Environ.env -> Evd.evar_map -> EConstr.type
 val pr_leconstr_core       : bool -> Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t
 val pr_lconstr_env         : env -> evar_map -> constr -> Pp.t
 
+(** Computes diffs for a single conclusion *)
+val diff_concl : ?og_s:goal sigma -> Evd.evar_map -> Goal.goal -> Pp.t
+
+(** Generates a map from [np] to [op] that maps changed goals to their prior
+forms.  The map doesn't include entries for unchanged goals; unchanged goals
+will have the same goal id in both versions.
+
+[op] and [np] must be from the same proof document and [op] must be for a state
+before [np]. *)
+val make_goal_map : Proof.t option -> Proof.t -> Evar.t Evar.Map.t
+
 (* Exposed for unit test, don't use these otherwise *)
 (* output channel for the test log file *)
 val log_out_ch : out_channel ref
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] *)