Merge PR #8247: Show diffs on multiple changed goals; match old and new goal info

13 files changed, 514 insertions, 143 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 f0ea6532de..67d71332b0 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 428dced117..518c5b930b 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/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/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] *)
 
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
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],