Merge PR #6801: Highlight differences between successive proof steps (color, underline, etc.)

31 files changed, 1862 insertions, 127 deletions

diff --git a/CHANGES b/CHANGES
index d642e8bd0d..f37ab8ae70 100644
--- a/CHANGES
+++ b/CHANGES
@@ -13,7 +13,7 @@ Tactics
 
 - The undocumented "nameless" forms `fix N`, `cofix` that were
   deprecated in 8.8 have been removed from LTAC's syntax; please use
-  `fix ident N/cofix ident` to explicitely name the (co)fixpoint
+  `fix ident N/cofix ident` to explicitly name the (co)fixpoint
   hypothesis to be introduced.
 
 - Introduction tactics "intro"/"intros" on a goal which is an
@@ -106,7 +106,7 @@ SSReflect
   In particular rule 3 lets one write {x}/v even if v uses the variable x:
   indeed the view is executed before the renaming.
 
-- An empty clear switch is now accepted in intro patterns before a 
+- An empty clear switch is now accepted in intro patterns before a
   view application whenever the view is a variable.
   One can now write {}/v to mean {v}/v.  Remark that {}/x is very similar
   to the idiom {}e for the rewrite tactic (the equation e is used for
@@ -117,6 +117,14 @@ Standard Library
 - There are now conversions between [string] and [positive], [Z],
   [nat], and [N] in binary, octal, and hex.
 
+Display diffs between proof steps
+
+- coqtop and coqide can now highlight the differences between proof steps
+  in color. This can be enabled from the command line or the
+  "Set Diffs on|off|removed" command. Please see the documentation for
+  details.  Showing diffs in Proof General requires small changes to PG
+  (under discussion).
+
 Changes from 8.8.0 to 8.8.1
 ===========================
 
diff --git a/clib/clib.mllib b/clib/clib.mllib
index afece4074c..5a2c9a9ce9 100644
--- a/clib/clib.mllib
+++ b/clib/clib.mllib
@@ -37,3 +37,5 @@ Backtrace
 IStream
 Terminal
 Monad
+
+Diff2
diff --git a/clib/diff2.ml b/clib/diff2.ml
new file mode 100644
index 0000000000..42c4733fed
--- /dev/null
+++ b/clib/diff2.ml
@@ -0,0 +1,158 @@
+(* copied from https://github.com/leque/ocaml-diff.git and renamed from "diff.ml" *)
+
+(*
+ * Copyright (C) 2016 OOHASHI Daichi
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy
+ * of this software and associated documentation files (the "Software"), to deal
+ * in the Software without restriction, including without limitation the rights
+ * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+ * copies of the Software, and to permit persons to whom the Software is
+ * furnished to do so, subject to the following conditions:
+ * The above copyright notice and this permission notice shall be included in
+ * all copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+ * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+ * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+ * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+ * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+ * THE SOFTWARE.
+ *)
+
+type 'a common =
+  [ `Common of int * int * 'a ]
+
+type 'a edit =
+  [ `Added of int * 'a
+  | `Removed of int * 'a
+  | 'a common
+  ]
+
+module type SeqType = sig
+  type t
+  type elem
+  val get : t -> int -> elem
+  val length : t -> int
+end
+
+module type S = sig
+  type t
+  type elem
+
+  val lcs :
+      ?equal:(elem -> elem -> bool) ->
+      t -> t -> elem common list
+
+  val diff :
+      ?equal:(elem -> elem -> bool) ->
+      t -> t -> elem edit list
+
+  val fold_left :
+      ?equal:(elem -> elem -> bool) ->
+      f:('a -> elem edit -> 'a) ->
+      init:'a ->
+      t -> t -> 'a
+
+  val iter :
+      ?equal:(elem -> elem -> bool) ->
+      f:(elem edit -> unit) ->
+      t -> t -> unit
+end
+
+module Make(M : SeqType) : (S with type t = M.t and type elem = M.elem) = struct
+  type t = M.t
+  type elem = M.elem
+
+  let lcs ?(equal = (=)) a b =
+    let n = M.length a in
+    let m = M.length b in
+    let mn = m + n in
+    let sz = 2 * mn + 1 in
+    let vd = Array.make sz 0 in
+    let vl = Array.make sz 0 in
+    let vr = Array.make sz [] in
+    let get v i = Array.get v (i + mn) in
+    let set v i x = Array.set v (i + mn) x in
+    let finish () =
+      let rec loop i maxl r =
+        if i > mn then
+          List.rev r
+        else if get vl i > maxl then
+          loop (i + 1) (get vl i) (get vr i)
+        else
+          loop (i + 1) maxl r
+      in loop (- mn) 0 []
+    in
+    if mn = 0 then
+      []
+    else
+      (* For d <- 0 to mn Do *)
+      let rec dloop d =
+        assert (d <= mn);
+        (* For k <- -d to d in steps of 2 Do *)
+        let rec kloop k =
+          if k > d then
+            dloop @@ d + 1
+          else
+            let x, l, r =
+              if k = -d || (k <> d && get vd (k - 1) < get vd (k + 1)) then
+                get vd (k + 1), get vl (k + 1), get vr (k + 1)
+              else
+                get vd (k - 1) + 1, get vl (k - 1), get vr (k - 1)
+            in
+            let x, y, l, r =
+              let rec xyloop x y l r =
+                if x < n && y < m && equal (M.get a x) (M.get b y) then
+                  xyloop (x + 1) (y + 1) (l + 1) (`Common(x, y, M.get a x) :: r)
+                else
+                  x, y, l, r
+              in xyloop x (x - k) l r
+            in
+            set vd k x;
+            set vl k l;
+            set vr k r;
+            if x >= n && y >= m then
+              (* Stop *)
+              finish ()
+            else
+              kloop @@ k + 2
+        in kloop @@ -d
+      in dloop 0
+
+  let fold_left ?(equal = (=)) ~f ~init a b =
+    let ff x y = f y x in
+    let fold_map f g x from to_ init =
+      let rec loop i init =
+        if i >= to_ then
+          init
+        else
+          loop (i + 1) (f (g i @@ M.get x i) init)
+      in loop from init
+    in
+    let added i x = `Added (i, x) in
+    let removed i x = `Removed (i, x) in
+    let rec loop cs apos bpos init =
+      match cs with
+      | [] ->
+          init
+          |> fold_map ff removed a apos (M.length a)
+          |> fold_map ff added b bpos (M.length b)
+      | `Common (aoff, boff, _) as e :: rest ->
+          init
+          |> fold_map ff removed a apos aoff
+          |> fold_map ff added b bpos boff
+          |> ff e
+          |> loop rest (aoff + 1) (boff + 1)
+    in loop (lcs ~equal a b) 0 0 init
+
+  let diff ?(equal = (=)) a b =
+    fold_left ~equal ~f:(fun xs x -> x::xs) ~init:[] a b
+
+  let iter ?(equal = (=)) ~f a b =
+    fold_left a b
+      ~equal
+      ~f:(fun () x -> f x)
+      ~init:()
+end
diff --git a/clib/diff2.mli b/clib/diff2.mli
new file mode 100644
index 0000000000..a085f4ffe8
--- /dev/null
+++ b/clib/diff2.mli
@@ -0,0 +1,101 @@
+(* copied from https://github.com/leque/ocaml-diff.git and renamed from "diff.mli" *)
+(**
+   An implementation of Eugene Myers' O(ND) Difference Algorithm\[1\].
+   This implementation is a port of util.lcs module of
+   {{:http://practical-scheme.net/gauche} Gauche Scheme interpreter}.
+
+   - \[1\] Eugene Myers, An O(ND) Difference Algorithm and Its Variations, Algorithmica Vol. 1 No. 2, pp. 251-266, 1986.
+ *)
+
+type 'a common = [
+    `Common of int * int * 'a
+  ]
+(** an element of lcs of seq1 and seq2 *)
+
+type 'a edit =
+  [ `Removed of int * 'a
+  | `Added of int * 'a
+  | 'a common
+  ]
+(** an element of diff of seq1 and seq2. *)
+
+module type SeqType = sig
+  type t
+  (** The type of the sequence. *)
+
+  type elem
+  (** The type of the elements of the sequence. *)
+
+  val get : t -> int -> elem
+  (** [get t n] returns [n]-th element of the sequence [t]. *)
+
+  val length : t -> int
+  (** [length t] returns the length of the sequence [t]. *)
+end
+(** Input signature of {!Diff.Make}. *)
+
+module type S = sig
+  type t
+  (** The type of input sequence. *)
+
+  type elem
+  (** The type of the elements of result / input sequence. *)
+
+  val lcs :
+      ?equal:(elem -> elem -> bool) ->
+      t -> t -> elem common list
+  (**
+     [lcs ~equal seq1 seq2] computes the LCS (longest common sequence) of
+     [seq1] and [seq2].
+     Elements of [seq1] and [seq2] are compared with [equal].
+     [equal] defaults to [Pervasives.(=)].
+
+     Elements of lcs are [`Common (pos1, pos2, e)]
+     where [e] is an element, [pos1] is a position in [seq1],
+     and [pos2] is a position in [seq2].
+   *)
+
+  val diff :
+      ?equal:(elem -> elem -> bool) ->
+      t -> t -> elem edit list
+  (**
+     [diff ~equal seq1 seq2] computes the diff of [seq1] and [seq2].
+     Elements of [seq1] and [seq2] are compared with [equal].
+
+     Elements only in [seq1] are represented as [`Removed (pos, e)]
+     where [e] is an element, and [pos] is a position in [seq1];
+     those only in [seq2] are represented as [`Added (pos, e)]
+     where [e] is an element, and [pos] is a position in [seq2];
+     those common in [seq1] and [seq2] are represented as
+     [`Common (pos1, pos2, e)]
+     where [e] is an element, [pos1] is a position in [seq1],
+     and [pos2] is a position in [seq2].
+   *)
+
+  val fold_left :
+      ?equal:(elem -> elem -> bool) ->
+      f:('a -> elem edit -> 'a) ->
+      init:'a ->
+      t -> t -> 'a
+  (**
+     [fold_left ~equal ~f ~init seq1 seq2] is same as
+     [diff ~equal seq1 seq2 |> ListLabels.fold_left ~f ~init],
+     but does not create an intermediate list.
+   *)
+
+  val iter :
+      ?equal:(elem -> elem -> bool) ->
+      f:(elem edit -> unit) ->
+      t -> t -> unit
+  (**
+     [iter ~equal ~f seq1 seq2] is same as
+     [diff ~equal seq1 seq2 |> ListLabels.iter ~f],
+     but does not create an intermediate list.
+   *)
+end
+(** Output signature of {!Diff.Make}. *)
+
+module Make :
+  functor (M : SeqType) -> (S with type t = M.t and type elem = M.elem)
+(** Functor building an implementation of the diff structure
+    given a sequence type.  *)
diff --git a/clib/terminal.ml b/clib/terminal.ml
index 1d9468137b..d243d6599e 100644
--- a/clib/terminal.ml
+++ b/clib/terminal.ml
@@ -59,6 +59,19 @@ let default = {
   suffix = None;
 }
 
+let reset = "\027[0m"
+
+let reset_style = {
+  fg_color = Some `DEFAULT;
+  bg_color = Some `DEFAULT;
+  bold = Some false;
+  italic = Some false;
+  underline = Some false;
+  negative = Some false;
+  prefix = None;
+  suffix = None;
+}
+
 let make ?fg_color ?bg_color ?bold ?italic ?underline ?negative ?style ?prefix ?suffix () =
   let st = match style with
   | None -> default
@@ -87,6 +100,25 @@ let merge s1 s2 =
     suffix = set s1.suffix s2.suffix;
   }
 
+let diff s1 s2 =
+  let diff_op o1 o2 reset_val = match o1 with
+  | None -> o2
+  | Some _ ->
+    match o2 with
+    | None -> reset_val
+    | Some _ -> if o1 = o2 then None else o2 in
+
+  {
+    fg_color = diff_op s1.fg_color s2.fg_color reset_style.fg_color;
+    bg_color = diff_op s1.bg_color s2.bg_color reset_style.bg_color;
+    bold = diff_op s1.bold s2.bold reset_style.bold;
+    italic = diff_op s1.italic s2.italic reset_style.italic;
+    underline = diff_op s1.underline s2.underline reset_style.underline;
+    negative = diff_op s1.negative s2.negative reset_style.negative;
+    prefix = diff_op s1.prefix s2.prefix reset_style.prefix;
+    suffix = diff_op s1.suffix s2.suffix reset_style.suffix;
+  }
+
 let base_color = function
 | `DEFAULT -> 9
 | `BLACK -> 0
@@ -167,20 +199,8 @@ let repr st =
 let eval st =
   let tags = repr st in
   let tags = List.map string_of_int tags in
-  Printf.sprintf "\027[%sm" (String.concat ";" tags)
-
-let reset = "\027[0m"
-
-let reset_style = {
-  fg_color = Some `DEFAULT;
-  bg_color = Some `DEFAULT;
-  bold = Some false;
-  italic = Some false;
-  underline = Some false;
-  negative = Some false;
-  prefix = None;
-  suffix = None;
-}
+  if List.length tags = 0 then "" else
+    Printf.sprintf "\027[%sm" (String.concat ";" tags)
 
 let has_style t =
   Unix.isatty t && Sys.os_type = "Unix"
diff --git a/clib/terminal.mli b/clib/terminal.mli
index dbf8d4640c..bc30b0016f 100644
--- a/clib/terminal.mli
+++ b/clib/terminal.mli
@@ -51,6 +51,9 @@ val make : ?fg_color:color -> ?bg_color:color ->
 val merge : style -> style -> style
 (** [merge s1 s2] returns [s1] with all defined values of [s2] overwritten. *)
 
+val diff : style -> style -> style
+(** [diff s1 s2] returns the differences between [s1] and [s2]. *)
+
 val repr : style -> int list
 (** Generate the ANSI code representing the given style. *)
 
@@ -60,6 +63,9 @@ val eval : style -> string
 val reset : string
 (** This escape sequence resets all attributes. *)
 
+val reset_style : style
+(** The default style *)
+
 val has_style : Unix.file_descr -> bool
 (** Whether an output file descriptor handles styles. Very heuristic, only
     checks it is a terminal. *)
diff --git a/ide/idetop.ml b/ide/idetop.ml
index 0c3328ee08..965bb913ff 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -202,13 +202,30 @@ 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 oldp =
+    try Some (Proof_global.give_me_the_proof ())
+    with Proof_global.NoCurrentProof -> None in
   let doc = get_doc () in
   set_doc @@ Stm.finish ~doc;
   try
-    let pfts = Proof_global.give_me_the_proof () in
-    Some (export_pre_goals (Proof.map_structured_proof pfts process_goal))
-  with Proof_global.NoCurrentProof -> None
+    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
+      try
+        Some (add_diffs oldp (Some newp) intf)
+      with Pp_diff.Diff_Failure _ -> Some intf
+    else
+      Some intf
+  with Proof_global.NoCurrentProof -> None;;
 
 let evars () =
   try
@@ -513,6 +530,9 @@ let () = Usage.add_to_usage "coqidetop"
 let islave_init ~opts extra_args =
   let args = parse extra_args in
   CoqworkmgrApi.(init High);
+  let open Coqargs in
+    if not opts.diffs_set then
+      Proof_diffs.write_diffs_option "on";
   opts, args
 
 let () =
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index e96b992999..960beb8455 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -37,6 +37,11 @@ let flash_info =
   let flash_context = status#new_context ~name:"Flash" in
     (fun ?(delay=5000) s -> flash_context#flash ~delay s)
 
+(* Note: Setting the same attribute with two separate tags appears to use
+the first value applied and not the second.  I saw this trying to set the background
+color on Windows.  A clean fix, if ever needed, would be to combine the attributes
+of the tags into a single composite tag before applying.  This is left as an
+exercise for the reader. *)
 let insert_with_tags (buf : #GText.buffer_skel) mark rmark tags text =
   (** FIXME: LablGTK2 does not export the C insert_with_tags function, so that
       it has to reimplement its own helper function. Unluckily, it relies on
@@ -50,21 +55,51 @@ let insert_with_tags (buf : #GText.buffer_skel) mark rmark tags text =
     let start = buf#get_iter_at_mark mark in
     let stop = buf#get_iter_at_mark rmark in
     let iter tag = buf#apply_tag tag ~start ~stop in
-    List.iter iter tags
+    List.iter iter (List.rev tags)
+
+let nl_white_regex = Str.regexp "^\\( *\n *\\)"
+let diff_regex = Str.regexp "^diff."
 
 let insert_xml ?(mark = `INSERT) ?(tags = []) (buf : #GText.buffer_skel) msg =
   let open Xml_datatype in
+  let dtags = ref [] in
   let tag name =
     match GtkText.TagTable.lookup buf#tag_table name with
     | None -> raise Not_found
     | Some tag -> new GText.tag tag
   in
   let rmark = `MARK (buf#create_mark buf#start_iter) in
+  (* insert the string, but don't apply diff highlights to white space at the begin/end of line *)
+  let rec insert_str tags s =
+    try
+      let _ = Str.search_forward nl_white_regex s 0 in
+      insert_with_tags buf mark rmark tags (Str.matched_group 1 s);
+      let mend = Str.match_end () in
+      insert_str tags (String.sub s mend (String.length s - mend))
+    with Not_found -> begin
+      let etags = try List.hd !dtags :: tags with hd -> tags in
+      insert_with_tags buf mark rmark etags s
+      end
+  in
   let rec insert tags = function
-  | PCData s -> insert_with_tags buf mark rmark tags s
+  | PCData s -> insert_str tags s
   | Element (t, _, children) ->
-    let tags = try tag t :: tags with Not_found -> tags in
-    List.iter (fun xml -> insert tags xml) children
+    let (pfx, tname) = Pp.split_tag t in
+    let is_diff = try let _ = Str.search_forward diff_regex tname 0 in true with Not_found -> false in
+    let (tags, have_tag) =
+      try
+        let t = tag tname in
+        if is_diff && pfx <> Pp.end_pfx then
+          dtags := t :: !dtags;
+        if pfx = "" then
+          ((if is_diff then tags else t :: tags), true)
+        else
+          (tags, true)
+      with Not_found -> (tags, false)
+    in
+    List.iter (fun xml -> insert tags xml) children;
+    if have_tag && is_diff && pfx <> Pp.start_pfx then
+      dtags := (try List.tl !dtags with tl -> []);
   in
   let () = try insert tags msg with _ -> () in
   buf#delete_mark rmark
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 11aaf6e8cc..526d94a939 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -25,6 +25,7 @@ type tag = {
   tag_bold : bool;
   tag_italic : bool;
   tag_underline : bool;
+  tag_strikethrough : bool;
 }
 
 (** Generic preferences *)
@@ -215,15 +216,17 @@ object
     string_of_bool tag.tag_bold;
     string_of_bool tag.tag_italic;
     string_of_bool tag.tag_underline;
+    string_of_bool tag.tag_strikethrough;
   ]
   method into = function
-  | [fg; bg; bd; it; ul] ->
+  | [fg; bg; bd; it; ul; st] ->
     (try Some {
       tag_fg_color = _to fg;
       tag_bg_color = _to bg;
       tag_bold = bool_of_string bd;
       tag_italic = bool_of_string it;
       tag_underline = bool_of_string ul;
+      tag_strikethrough = bool_of_string st;
       }
     with _ -> None)
   | _ -> None
@@ -429,12 +432,13 @@ let tags = ref Util.String.Map.empty
 
 let list_tags () = !tags
 
-let make_tag ?fg ?bg ?(bold = false) ?(italic = false) ?(underline = false) () = {
+let make_tag ?fg ?bg ?(bold = false) ?(italic = false) ?(underline = false) ?(strikethrough = false) () = {
   tag_fg_color = fg;
   tag_bg_color = bg;
   tag_bold = bold;
   tag_italic = italic;
   tag_underline = underline;
+  tag_strikethrough = strikethrough;
 }
 
 let create_tag name default =
@@ -470,6 +474,12 @@ let create_tag name default =
       tag#set_property (`UNDERLINE_SET true);
       tag#set_property (`UNDERLINE `SINGLE)
     end;
+    begin match pref#get.tag_strikethrough with
+    | false -> tag#set_property (`STRIKETHROUGH_SET false)
+    | true ->
+      tag#set_property (`STRIKETHROUGH_SET true);
+      tag#set_property (`STRIKETHROUGH true)
+    end;
   in
   let iter table =
     let tag = GText.tag ~name () in
@@ -480,6 +490,8 @@ let create_tag name default =
   List.iter iter [Tags.Script.table; Tags.Proof.table; Tags.Message.table];
   tags := Util.String.Map.add name pref !tags
 
+(* note these appear to only set the defaults; they don't override
+the user selection from the Edit/Preferences/Tags dialog *)
 let () =
   let iter (name, tag) = create_tag name tag in
   List.iter iter [
@@ -498,6 +510,10 @@ let () =
     ("tactic.keyword", make_tag ());
     ("tactic.primitive", make_tag ());
     ("tactic.string", make_tag ());
+    ("diff.added", make_tag ~bg:"#b6f1c0" ~underline:true ());
+    ("diff.removed", make_tag ~bg:"#f6b9c1" ~strikethrough:true ());
+    ("diff.added.bg", make_tag ~bg:"#e9feee" ());
+    ("diff.removed.bg", make_tag ~bg:"#fce9eb" ());
   ]
 
 let processed_color =
@@ -561,6 +577,7 @@ object (self)
   val bold = GButton.toggle_button ()
   val italic = GButton.toggle_button ()
   val underline = GButton.toggle_button ()
+  val strikethrough = GButton.toggle_button ()
 
   method set_tag tag =
     let track c but set = match c with
@@ -574,6 +591,7 @@ object (self)
     bold#set_active tag.tag_bold;
     italic#set_active tag.tag_italic;
     underline#set_active tag.tag_underline;
+    strikethrough#set_active tag.tag_strikethrough;
 
   method tag =
     let get but set =
@@ -586,6 +604,7 @@ object (self)
       tag_bold = bold#active;
       tag_italic = italic#active;
       tag_underline = underline#active;
+      tag_strikethrough = strikethrough#active;
     }
 
   initializer
@@ -599,6 +618,7 @@ object (self)
     set_stock bold `BOLD;
     set_stock italic `ITALIC;
     set_stock underline `UNDERLINE;
+    set_stock strikethrough `STRIKETHROUGH;
     box#pack fg_color#coerce;
     box#pack fg_unset#coerce;
     box#pack bg_color#coerce;
@@ -606,6 +626,7 @@ object (self)
     box#pack bold#coerce;
     box#pack italic#coerce;
     box#pack underline#coerce;
+    box#pack strikethrough#coerce;
     let cb but obj = obj#set_sensitive (not but#active) in
     let _ = fg_unset#connect#toggled ~callback:(fun () -> cb fg_unset fg_color#misc) in
     let _ = bg_unset#connect#toggled ~callback:(fun () -> cb bg_unset bg_color#misc) in
diff --git a/ide/preferences.mli b/ide/preferences.mli
index ccf028aee4..f3882d486d 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -21,6 +21,7 @@ type tag = {
   tag_bold : bool;
   tag_italic : bool;
   tag_underline : bool;
+  tag_strikethrough : bool;
 }
 
 class type ['a] repr =
diff --git a/lib/lib.mllib b/lib/lib.mllib
index 0891859423..41b3622a99 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -6,6 +6,7 @@ Control
 Util
 
 Pp
+Pp_diff
 Stateid
 Loc
 Feedback
diff --git a/lib/pp.ml b/lib/pp.ml
index cd81f6e768..7f132686db 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -139,7 +139,7 @@ let v   n s = Ppcmd_box(Pp_vbox n,s)
 let hv  n s = Ppcmd_box(Pp_hvbox n,s)
 let hov n s = Ppcmd_box(Pp_hovbox n,s)
 
-(* Opening and closed of tags *)
+(* Opening and closing of tags *)
 let tag t s = Ppcmd_tag(t,s)
 
 (* In new syntax only double quote char is escaped by repeating it *)
@@ -167,6 +167,20 @@ let rec pr_com ft s =
       Some s2 -> Format.pp_force_newline ft (); pr_com ft s2
     | None -> ()
 
+let start_pfx = "start."
+let end_pfx = "end."
+
+let split_pfx pfx str =
+  let (str_len, pfx_len) = (String.length str, String.length pfx) in
+  if str_len >= pfx_len && (String.sub str 0 pfx_len) = pfx then
+    (pfx, String.sub str pfx_len (str_len - pfx_len)) else ("", str);;
+
+let split_tag tag =
+  let (pfx, ttag) = split_pfx start_pfx tag in
+  if pfx <> "" then (pfx, ttag) else
+    let (pfx, ttag) = split_pfx end_pfx tag in
+    (pfx, ttag);;
+
 (* pretty printing functions *)
 let pp_with ft pp =
   let cpp_open_box = function
@@ -297,3 +311,62 @@ let prvect_with_sep sep elem v = prvecti_with_sep sep (fun _ -> elem) v
 let prvect elem v = prvect_with_sep mt elem v
 
 let surround p = hov 1 (str"(" ++ p ++ str")")
+
+(*** DEBUG code ***)
+
+let db_print_pp fmt pp =
+  let open Format in
+  let block_type fmt btype =
+    let (bt, v) =
+      match btype with
+      | Pp_hbox v -> ("Pp_hbox", v)
+      | Pp_vbox v -> ("Pp_vbox", v)
+      | Pp_hvbox v -> ("Pp_hvbox", v)
+      | Pp_hovbox v -> ("Pp_hovbox", v)
+    in
+    fprintf fmt "%s %d" bt v
+  in
+  let rec db_print_pp_r indent pp =
+    let ind () = fprintf fmt "%s" (String.make (2 * indent) ' ') in
+    ind();
+    match pp with
+    | Ppcmd_empty ->
+        fprintf fmt "Ppcmd_empty@;"
+    | Ppcmd_string str ->
+        fprintf fmt "Ppcmd_string '%s'@;" str
+    | Ppcmd_glue list ->
+        fprintf fmt "Ppcmd_glue@;";
+        List.iter (fun x -> db_print_pp_r (indent + 1) (repr x)) list;
+    | Ppcmd_box (block, pp) ->
+        fprintf fmt "Ppcmd_box %a@;" block_type block;
+        db_print_pp_r (indent + 1) (repr pp);
+    | Ppcmd_tag (tag, pp) ->
+        fprintf fmt "Ppcmd_tag %s@;" tag;
+        db_print_pp_r (indent + 1) (repr pp);
+    | Ppcmd_print_break (i, j) ->
+        fprintf fmt "Ppcmd_print_break %d %d@;" i j
+    | Ppcmd_force_newline ->
+        fprintf fmt "Ppcmd_force_newline@;"
+    | Ppcmd_comment list ->
+        fprintf fmt "Ppcmd_comment@;";
+        List.iter (fun x -> ind(); (fprintf fmt "%s@;" x)) list
+  in
+  pp_open_vbox fmt 0;
+  db_print_pp_r 0 pp;
+  pp_close_box fmt ();
+  pp_print_flush fmt ()
+
+let db_string_of_pp pp =
+  Format.asprintf "%a" db_print_pp pp
+
+let rec flatten pp =
+  match pp with
+  | Ppcmd_glue l -> Ppcmd_glue (List.concat (List.map
+      (fun x -> let x = flatten x in
+                  match x with
+                  | Ppcmd_glue l2 -> l2
+                  | p -> [p])
+      l))
+  | Ppcmd_box (block, pp) -> Ppcmd_box (block, flatten pp)
+  | Ppcmd_tag (tag, pp) -> Ppcmd_tag (tag, flatten pp)
+  | p -> p
diff --git a/lib/pp.mli b/lib/pp.mli
index f3a0a29b8a..ed31daa561 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -189,3 +189,22 @@ val pr_vertical_list : ('b -> t) -> 'b list -> t
 val pp_with          : Format.formatter -> t -> unit
 
 val string_of_ppcmds : t -> string
+
+
+(** Tag prefix to start a multi-token diff span *)
+val start_pfx : string
+
+(** Tag prefix to end a multi-token diff span *)
+val end_pfx : string
+
+(** Split a tag into prefix and base tag *)
+val split_tag : string -> string * string
+
+(** Print the Pp in tree form for debugging *)
+val db_print_pp : Format.formatter -> t -> unit
+
+(** Print the Pp in tree form for debugging, return as a string *)
+val db_string_of_pp : t -> string
+
+(** Combine nested Ppcmd_glues *)
+val flatten : t -> t
diff --git a/lib/pp_diff.ml b/lib/pp_diff.ml
new file mode 100644
index 0000000000..7b4b1eab73
--- /dev/null
+++ b/lib/pp_diff.ml
@@ -0,0 +1,303 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* DEBUG/UNIT TEST *)
+let cfprintf oc = Printf.(kfprintf (fun oc -> fprintf oc "") oc)
+let log_out_ch = ref stdout
+let cprintf s = cfprintf !log_out_ch s
+
+
+module StringDiff = Diff2.Make(struct
+  type elem = String.t
+  type t = elem array
+  let get t i = Array.get t i
+  let length t = Array.length t
+end)
+
+type diff_type =
+  [ `Removed
+  | `Added
+  | `Common
+  ]
+
+type diff_list = StringDiff.elem Diff2.edit list
+
+(* debug print diff data structure *)
+let db_print_diffs fmt diffs =
+  let open Format in
+  let print_diff = function
+    | `Common (opos, npos, s) ->
+      fprintf fmt "Common '%s' opos = %d npos = %d\n" s opos npos;
+    | `Removed (pos, s) ->
+      fprintf fmt "Removed '%s' opos = %d\n" s pos;
+    | `Added (pos, s) ->
+      fprintf fmt "Added '%s' npos = %d\n" s pos;
+  in
+  pp_open_vbox fmt 0;
+  List.iter print_diff diffs;
+  pp_close_box fmt ();
+  pp_print_flush fmt ()
+
+let string_of_diffs diffs =
+  Format.asprintf "%a" db_print_diffs diffs
+
+(* Adjust the diffs returned by the Myers algorithm to reduce the span of the
+changes.  This gives more natural-looking diffs.
+
+While the Myers algorithm minimizes the number of changes between two
+sequences, it doesn't minimize the span of the changes.  For example,
+representing elements in common in lower case and inserted elements in upper
+case (but ignoring case in the algorithm), ABabC and abABC both have 3 changes
+(A, B and C).  However the span of the first sequence is 5 elements (ABabC)
+while the span of the second is 3 elements (ABC).
+
+The algorithm modifies the changes iteratively, for example ABabC -> aBAbC -> abABC
+
+dtype: identifies which of Added OR Removed to use; the other one is ignored.
+diff_list: output from the Myers algorithm
+*)
+let shorten_diff_span dtype diff_list =
+  let changed = ref false in
+  let diffs = Array.of_list diff_list in
+  let len = Array.length diffs in
+  let vinfo index =
+    match diffs.(index) with
+    | `Common (opos, npos, s) -> (`Common, opos, npos, s)
+    | `Removed (pos, s) -> (`Removed, pos, 0, s)
+    | `Added (pos, s) -> (`Added, 0, pos, s) in
+  let get_variant index =
+    let (v, _, _, _) = vinfo index in
+    v in
+  let get_str index =
+    let (_, _, _, s) = vinfo index in
+    s in
+
+  let iter start len lt incr = begin
+    let src = ref start in
+    let dst = ref start in
+    while (lt !src len) do
+      if (get_variant !src) = dtype then begin
+        if (lt !dst !src) then
+          dst := !src;
+        while (lt !dst len) && (get_variant !dst) <> `Common do
+          dst := !dst + incr;
+        done;
+        if (lt !dst len) && (get_str !src) = (get_str !dst) then begin
+          (* swap diff *)
+          let (_, c_opos, c_npos, str) = vinfo !dst
+          and (_, v_opos, v_npos, _) = vinfo !src in
+          changed := true;
+          if dtype = `Added then begin
+            diffs.(!src) <- `Common (c_opos, v_npos, str);
+            diffs.(!dst) <- `Added (c_npos, str);
+          end else begin
+            diffs.(!src) <- `Common (v_opos, c_npos, str);
+            diffs.(!dst) <- `Removed (c_opos, str)
+          end
+        end
+      end;
+      src := !src + incr
+    done
+  end in
+
+  iter 0 len (<) 1; (* left to right *)
+  iter (len-1) (-1) (>) (-1); (* right to left *)
+  if !changed then Array.to_list diffs else diff_list;;
+
+let has_changes diffs =
+  let rec has_changes_r diffs added removed =
+    match diffs with
+    | `Added _ :: t   -> has_changes_r t true removed
+    | `Removed _ :: t -> has_changes_r t added true
+    | h :: t -> has_changes_r t added removed
+    | [] -> (added, removed) in
+  has_changes_r diffs false false;;
+
+(* get the Myers diff of 2 lists of strings *)
+let diff_strs old_strs new_strs =
+  let diffs = List.rev (StringDiff.diff old_strs new_strs) in
+  shorten_diff_span `Removed (shorten_diff_span `Added diffs);;
+
+(* Default string tokenizer.  Makes each character a separate strin.
+Whitespace is not ignored.  Doesn't handle UTF-8 differences well. *)
+let def_tokenize_string s =
+  let limit = (String.length s) - 1 in
+  let strs : string list ref = ref [] in
+  for i = 0 to limit do
+    strs := (String.make 1 s.[i]) :: !strs
+  done;
+  List.rev !strs
+
+(* get the Myers diff of 2 strings *)
+let diff_str ?(tokenize_string=def_tokenize_string) old_str new_str =
+  let old_toks = Array.of_list (tokenize_string old_str)
+  and new_toks = Array.of_list (tokenize_string new_str) in
+  diff_strs old_toks new_toks;;
+
+let get_dinfo = function
+  | `Common (_, _, s) -> (`Common, s)
+  | `Removed (_, s) -> (`Removed, s)
+  | `Added (_, s) -> (`Added, s)
+
+[@@@ocaml.warning "-32"]
+let string_of_diff_type = function
+  | `Common  -> "Common"
+  | `Removed -> "Removed"
+  | `Added -> "Added"
+[@@@ocaml.warning "+32"]
+
+let wrap_in_bg diff_tag pp =
+  let open Pp in
+  (tag (Pp.start_pfx ^ diff_tag ^ ".bg") (str "")) ++ pp ++
+  (tag (Pp.end_pfx   ^ diff_tag ^ ".bg") (str ""))
+
+exception Diff_Failure of string
+
+let add_diff_tags which pp diffs  =
+  let open Pp in
+  let diff_tag = if which = `Added then "diff.added" else "diff.removed" in
+  let diffs : diff_list ref = ref diffs in
+  let in_diff = ref false in (* true = buf chars need a tag *)
+  let in_span = ref false in (* true = last pp had a start tag *)
+  let trans = ref false in   (* true = this diff starts/ends highlight *)
+  let buf = Buffer.create 16 in
+  let acc_pp = ref [] in
+  let diff_str, diff_ind, diff_len = ref "", ref 0, ref 0 in
+  let prev_dtype, dtype, next_dtype = ref `Common, ref `Common, ref `Common in
+  let is_white c = List.mem c [' '; '\t'; '\n'; '\r'] in
+
+  let skip () =
+    while !diffs <> [] &&
+      (let (t, _) = get_dinfo (List.hd !diffs) in
+        t <> `Common && t <> which)
+    do
+      diffs := List.tl !diffs
+    done
+  in
+
+  let put_tagged case =
+    if Buffer.length buf > 0 then begin
+      let pp = str (Buffer.contents buf) in
+      Buffer.clear buf;
+      let tagged = match case with
+      | ""      -> pp
+      | "tag"   -> tag diff_tag pp
+      | "start" -> in_span := true;  tag (start_pfx ^ diff_tag) pp
+      | "end"   -> in_span := false; tag (end_pfx ^ diff_tag) pp
+      | _ -> raise (Diff_Failure "invalid tag id in put_tagged, should be impossible") in
+      acc_pp := tagged :: !acc_pp
+    end
+  in
+
+  let output_pps () =
+    let next_diff_char_hl = if !diff_ind < !diff_len then !dtype = which else !next_dtype = which in
+    let tag = if not !in_diff then ""
+              else  if !in_span then
+                      if next_diff_char_hl then "" else "end"
+                    else
+                      if next_diff_char_hl then "start" else "tag" in
+    put_tagged tag;  (* flush any remainder *)
+    let l = !acc_pp in
+    acc_pp := [];
+    match List.length l with
+    | 0 -> str ""
+    | 1 -> List.hd l
+    | _ -> seq (List.rev l)
+  in
+
+  let maybe_next_diff () =
+    if !diff_ind = !diff_len && (skip(); !diffs <> []) then begin
+      let (t, s) = get_dinfo (List.hd !diffs) in
+      diff_str := s; diff_ind := 0; diff_len := String.length !diff_str;
+      diffs := List.tl !diffs; skip();
+      prev_dtype := !dtype;
+      dtype := t;
+      next_dtype := (match !diffs with
+        | diff2 :: _ -> let (nt, _) = get_dinfo diff2 in nt
+        | [] -> `Common);
+      trans := !dtype <> !prev_dtype
+    end;
+  in
+
+  let s_char c =
+    maybe_next_diff ();
+    (* matching first should handle tokens with spaces, e.g. in comments/strings *)
+    if !diff_ind < !diff_len && c = !diff_str.[!diff_ind] then begin
+      if !dtype = which && !trans && !diff_ind = 0 then begin
+        put_tagged "";
+        in_diff := true
+      end;
+      Buffer.add_char buf c;
+      diff_ind := !diff_ind + 1;
+      if !dtype = which && !dtype <> !next_dtype && !diff_ind = !diff_len then begin
+        put_tagged (if !in_span then "end" else "tag");
+        in_diff := false
+      end
+    end else if is_white c then
+      Buffer.add_char buf c
+    else begin
+      cprintf "mismatch: expected '%c' but got '%c'\n" !diff_str.[!diff_ind] c;
+      raise (Diff_Failure "string mismatch, shouldn't happen")
+    end
+  in
+
+  (* rearrange so existing tags are inside diff tags, provided that those tags
+    only contain Ppcmd_string's.  Other cases (e.g. tag of a box) are not supported. *)
+  (* todo: Is there a better way to do this in OCaml without multiple 'repr's? *)
+  let reorder_tags child pp_tag pp =
+    match repr child with
+    | Ppcmd_tag (t1, pp) -> tag t1 (tag pp_tag pp)
+    | Ppcmd_glue l ->
+      if List.exists (fun x ->
+          match repr x with
+          | Ppcmd_tag (_, _) -> true
+          | _ -> false)  l
+      then seq (List.map (fun x ->
+          match repr x with
+          | Ppcmd_tag (t2, pp2) -> tag t2 (tag pp_tag pp2)
+          | pp2 -> tag pp_tag (unrepr pp2))   l)
+      else child
+    | _ -> tag pp_tag child
+  in
+
+  let rec add_tags_r pp =
+    let r_pp = repr pp in
+    match r_pp with
+    | Ppcmd_string s -> String.iter s_char s; output_pps ()
+    | Ppcmd_glue l -> seq (List.map add_tags_r l)
+    | Ppcmd_box (block_type, pp) -> unrepr (Ppcmd_box (block_type, add_tags_r pp))
+    | Ppcmd_tag (pp_tag, pp) -> reorder_tags (add_tags_r pp) pp_tag pp
+    | _ -> pp
+  in
+  let (has_added, has_removed) = has_changes !diffs in
+  let rv = add_tags_r pp in
+  skip ();
+  if !diffs <> [] then
+    raise (Diff_Failure "left-over diff info at end of Pp.t, should be impossible");
+  if has_added || has_removed then wrap_in_bg diff_tag rv else rv;;
+
+let diff_pp ?(tokenize_string=def_tokenize_string) o_pp n_pp =
+  let open Pp in
+  let o_str = string_of_ppcmds o_pp in
+  let n_str = string_of_ppcmds n_pp in
+  let diffs = diff_str ~tokenize_string o_str n_str in
+  (add_diff_tags `Removed o_pp diffs, add_diff_tags `Added n_pp diffs);;
+
+let diff_pp_combined ?(tokenize_string=def_tokenize_string) ?(show_removed=false) o_pp n_pp =
+  let open Pp in
+  let o_str = string_of_ppcmds o_pp in
+  let n_str = string_of_ppcmds n_pp in
+  let diffs = diff_str ~tokenize_string o_str n_str in
+  let (_, has_removed) = has_changes diffs in
+  let added = add_diff_tags `Added n_pp diffs in
+  if show_removed && has_removed then
+    let removed = add_diff_tags `Removed o_pp diffs in
+    (v 0 (removed ++ cut() ++ added))
+  else added;;
diff --git a/lib/pp_diff.mli b/lib/pp_diff.mli
new file mode 100644
index 0000000000..03468271d2
--- /dev/null
+++ b/lib/pp_diff.mli
@@ -0,0 +1,116 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(**
+Computes the differences between 2 Pp's and adds additional tags to a Pp
+to highlight them.  Strings are split into tokens using the Coq lexer,
+then the lists of tokens are diffed using the Myers algorithm.  A fixup routine,
+shorten_diff_span, shortens the span of the diff result in some cases.
+
+Highlights use 4 tags to specify the color and underline/strikeout.  These are
+"diffs.added", "diffs.removed", "diffs.added.bg" and "diffs.removed.bg".  The
+first two are for added or removed text; the last two are for unmodified parts
+of a modified item.  Diffs that span multiple strings in the Pp are tagged with
+"start.diff.*" and "end.diff.*", but only on the first and last strings of the span.
+
+If the inputs are not acceptable to the lexer, break the strings into
+lists of tokens and call diff_strs, then add_diff_tags with a Pp.t that matches
+the input lists of strings.  Tokens that the lexer doesn't return exactly as they
+appeared in the input will raise an exception in add_diff_tags (e.g. comments
+and quoted strings).  Fixing that requires tweaking the lexer.
+
+Limitations/Possible enhancements:
+
+- Make diff_pp immune to unlexable strings by adding a flag to the lexer.
+*)
+
+(** Compute the diff between two Pp.t structures and return
+versions of each with diffs highlighted as (old, new) *)
+val diff_pp : ?tokenize_string:(string -> string list) -> Pp.t -> Pp.t -> Pp.t * Pp.t
+
+(** Compute the diff between two Pp.t structures and return
+a highlighted Pp.t.  If [show_removed] is true, show separate lines for
+removals and additions, otherwise only show additions *)
+val diff_pp_combined : ?tokenize_string:(string -> string list) -> ?show_removed:bool -> Pp.t -> Pp.t -> Pp.t
+
+(** Raised if the diff fails *)
+exception Diff_Failure of string
+
+module StringDiff :
+sig
+  type elem = String.t
+  type t = elem array
+end
+
+type diff_type =
+  [ `Removed
+  | `Added
+  | `Common
+  ]
+
+type diff_list = StringDiff.elem Diff2.edit list
+
+(** Compute the difference between 2 strings in terms of tokens, using the
+lexer to identify tokens.
+
+If the strings are not lexable, this routine will raise Diff_Failure.
+(I expect to modify the lexer soon so this won't happen.)
+
+Therefore you should catch any exceptions.  The workaround for now is for the
+caller to tokenize the strings itself and then call diff_strs.
+*)
+val diff_str : ?tokenize_string:(string -> string list) -> string -> string -> StringDiff.elem Diff2.edit list
+
+(** Compute the differences between 2 lists of strings, treating the strings
+in the lists as indivisible units.
+*)
+val diff_strs : StringDiff.t -> StringDiff.t -> StringDiff.elem Diff2.edit list
+
+(** Generate a new Pp that adds tags marking diffs to a Pp structure:
+which: either `Added or `Removed, indicates which type of diffs to add
+pp: the original structure. For `Added, must be the new pp passed to diff_pp
+  For `Removed, must be the old pp passed to diff_pp.  Passing the wrong one
+  will likely raise Diff_Failure.
+diffs: the diff list returned by diff_pp
+
+Diffs of single strings in the Pp are tagged with "diff.added" or "diff.removed".
+Diffs that span multiple strings in the Pp are tagged with "start.diff.*" or
+"end.diff.*", but only on the first and last strings of the span.
+
+Ppcmd_strings will be split into multiple Ppcmd_strings if a diff starts or ends
+in the middle of the string.  Whitespace just before or just after a diff will
+not be part of the highlight.
+
+Prexisting tags in pp may contain only a single Ppcmd_string.  Those tags will be
+placed inside the diff tags to ensure proper nesting of tags within spans of
+"start.diff.*" ... "end.diff.*".
+
+Under some  "impossible" conditions, this routine may raise Diff_Failure.
+If you want to make your call especially bulletproof, catch this
+exception, print a user-visible message, then recall this routine with
+the first argument set to None, which will skip the diff.
+*)
+val add_diff_tags : diff_type -> Pp.t -> StringDiff.elem Diff2.edit list -> Pp.t
+
+(** Returns a boolean pair (added, removed) for [diffs] where a true value
+indicates that something was added/removed in the diffs.
+*)
+val has_changes : diff_list -> bool * bool
+
+val get_dinfo : StringDiff.elem Diff2.edit -> diff_type * string
+
+(** Returns a modified [pp] with the background highlighted with
+"start.<diff_tag>.bg" and "end.<diff_tag>.bg" tags at the beginning
+and end of the returned Pp.t
+*)
+val wrap_in_bg : string -> Pp.t -> Pp.t
+
+(** Displays the diffs to a printable format for debugging *)
+val string_of_diffs : diff_list -> string
diff --git a/printing/printer.ml b/printing/printer.ml
index 92224c992c..ba094596ff 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -493,16 +493,23 @@ let pr_transparent_state (ids, csts) =
   hv 0 (str"VARIABLES: " ++ pr_idpred ids ++ fnl () ++
 	str"CONSTANTS: " ++ pr_cpred csts ++ fnl ())
 
-(* display complete goal *)
-let pr_goal gs =
+(* display complete goal
+ prev_gs has info on the previous proof step for diffs
+ gs has info 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 env = Goal.V82.env sigma g in
   let concl = Goal.V82.concl sigma g in
   let goal =
-    pr_context_of env sigma ++ cut () ++
-      str "============================" ++ cut ()  ++
-      pr_goal_concl_style_env env sigma concl in
+    if diffs then
+      Proof_diffs.diff_goals ?prev_gs (Some gs)
+    else
+      pr_context_of env sigma ++ cut () ++
+        str "============================" ++ cut ()  ++
+        pr_goal_concl_style_env env sigma concl
+  in
   str "  " ++ v 0 goal
 
 (* display a goal tag *)
@@ -695,7 +702,8 @@ let print_dependent_evars gl sigma seeds =
 (* 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. *)
-let pr_subgoals ?(pr_first=true)
+(* [prev] is the previous proof step, used for diffs *)
+let pr_subgoals ?(pr_first=true) ?(diffs=false) ?prev
                         close_cmd sigma ~seeds ~shelf ~stack ~unfocused ~goals =
   (** Printing functions for the extra informations. *)
   let rec print_stack a = function
@@ -729,7 +737,7 @@ let pr_subgoals ?(pr_first=true)
     if needed then str" focused "
     else str" " (* non-breakable space *)
   in
-  (** Main function *)
+
   let rec pr_rec n = function
     | [] -> (mt ())
     | g::rest ->
@@ -739,7 +747,14 @@ let pr_subgoals ?(pr_first=true)
   in
   let print_multiple_goals g l =
     if pr_first then
-      pr_goal { it = g ; sigma = sigma; }
+      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 }
       ++ (if l=[] then mt () else cut ())
       ++ pr_rec 2 l
     else 
@@ -751,6 +766,8 @@ let pr_subgoals ?(pr_first=true)
     | Some cmd -> Feedback.msg_info cmd
     | None -> ()
   in
+
+  (** Main function *)
   match goals with
   | [] ->
       begin
@@ -780,7 +797,7 @@ let pr_subgoals ?(pr_first=true)
 	++ print_dependent_evars (Some g1) sigma seeds
       )
 
-let pr_open_subgoals ~proof =
+let pr_open_subgoals_diff ?(quiet=false) ?(diffs=false) ?prev_proof 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
@@ -803,21 +820,33 @@ let pr_open_subgoals ~proof =
 	    fnl ()
             ++ pr_subgoals ~pr_first:false None bsigma ~seeds ~shelf:[] ~stack:[] ~unfocused:[] ~goals:shelf
 	  | _ , _, _ ->
-            let end_cmd =
-              str "This subproof is complete, but there are some unfocused goals." ++
-              (let s = Proof_bullet.suggest p in
-               if Pp.ismt s then s else fnl () ++ s) ++
-              fnl ()
+            let cmd = if quiet then None else
+              Some
+                (str "This subproof is complete, but there are some unfocused goals." ++
+                (let s = Proof_bullet.suggest p in
+                 if Pp.ismt s then s else fnl () ++ s) ++
+                fnl ())
             in
-            pr_subgoals ~pr_first:false (Some end_cmd) bsigma ~seeds ~shelf ~stack:[] ~unfocused:[] ~goals:bgoals
+            pr_subgoals ~pr_first:false cmd bsigma ~seeds ~shelf ~stack:[] ~unfocused:[] ~goals:bgoals
 	  end
   | _ -> 
      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
-     pr_subgoals ~pr_first:true None bsigma ~seeds ~shelf ~stack:[] ~unfocused:unfocused_if_needed ~goals:bgoals_focused
+     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
+     in
+     pr_subgoals ~pr_first:true ~diffs ?prev None bsigma ~seeds ~shelf ~stack:[] ~unfocused:unfocused_if_needed ~goals:bgoals_focused
   end
 
+let pr_open_subgoals ~proof =
+  pr_open_subgoals_diff proof
+
 let pr_nth_open_subgoal ~proof n =
   let gls,_,_,_,sigma = Proof.proof proof in
   pr_subgoal n sigma gls
@@ -990,3 +1019,30 @@ let pr_polymorphic b =
 let pr_universe_instance evd ctx =
   let inst = Univ.UContext.instance ctx in
     str"@{" ++ Univ.Instance.pr (Termops.pr_evd_level evd) inst ++ str"}"
+
+(* print the proof step, possibly with diffs highlighted, *)
+let print_and_diff oldp newp =
+  match newp with
+  | None -> ()
+  | Some proof ->
+    let output =
+      if Proof_diffs.show_diffs () then
+        try pr_open_subgoals_diff ~diffs:true ?prev_proof: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" ));
+          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 eddfef6fad..948b06f3f6 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -171,22 +171,26 @@ val pr_transparent_state   : transparent_state -> Pp.t
 
 (** Proofs, these functions obey [Hyps Limit] and [Compact contexts]. *)
 
-val pr_goal                : goal sigma -> Pp.t
+val pr_goal                : ?diffs:bool -> ?prev_gs:(goal sigma) -> goal sigma -> Pp.t
 
-(** [pr_subgoals ~pr_first pp sigma seeds shelf focus_stack unfocused goals]
+(** [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. This function can be
-   replaced by another one by calling [set_printer_pr] (see below),
-   typically by plugin writers. The default printer prints only the
+   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 -> Pp.t option -> evar_map -> seeds:goal list -> shelf:goal list -> stack:int list -> unfocused:goal list -> goals:goal list -> Pp.t
+val pr_subgoals            : ?pr_first:bool -> ?diffs:bool -> ?prev:(goal list * evar_map) -> 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
 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
@@ -197,6 +201,8 @@ val pr_ne_evar_set         : Pp.t -> Pp.t -> evar_map ->
 
 val pr_prim_rule           : prim_rule -> Pp.t
 
+val print_and_diff : Proof.t option -> Proof.t option -> unit
+
 (** Backwards compatibility *)
 
 val prterm                 : constr -> Pp.t (** = pr_lconstr *)
diff --git a/printing/printing.mllib b/printing/printing.mllib
index b69d8a9ef8..deb52ad270 100644
--- a/printing/printing.mllib
+++ b/printing/printing.mllib
@@ -1,6 +1,7 @@
 Genprint
 Pputils
 Ppconstr
+Proof_diffs
 Printer
 Printmod
 Prettyp
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
new file mode 100644
index 0000000000..7131ced15b
--- /dev/null
+++ b/printing/proof_diffs.ml
@@ -0,0 +1,339 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(*
+Displays the differences between successive proof steps in coqtop and CoqIDE.
+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 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.
+
+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
+uses strikeout on removed text.
+*)
+
+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"
+| `REMOVED -> "removed"
+
+let write_diffs_option = function
+| "off" -> diff_option := `OFF
+| "on" -> diff_option := `ON
+| "removed" -> diff_option := `REMOVED
+| _ -> CErrors.user_err Pp.(str "Diffs option only accepts the following values: \"off\", \"on\", \"removed\".")
+
+let _ =
+  Goptions.(declare_string_option {
+    optdepr = false;
+    optname = "show diffs in proofs";
+    optkey = ["Diffs"];
+    optread = read_diffs_option;
+    optwrite = write_diffs_option
+  })
+
+let show_diffs () = !diff_option <> `OFF;;
+let show_removed () = !diff_option = `REMOVED;;
+
+
+(* DEBUG/UNIT TEST *)
+let cfprintf oc = Printf.(kfprintf (fun oc -> fprintf oc "") oc)
+let log_out_ch = ref stdout
+[@@@ocaml.warning "-32"]
+let cprintf s = cfprintf !log_out_ch s
+[@@@ocaml.warning "+32"]
+
+module StringMap = Map.Make(String);;
+
+let tokenize_string s =
+  (* todo: cLexer changes buff as it proceeds.  Seems like that should be saved, too.
+  But I don't understand how it's used--it looks like things get appended to it but
+  it never gets cleared. *)
+  let rec stream_tok acc str =
+    let e = Stream.next str in
+    if Tok.(equal e EOI) then
+      List.rev acc
+    else
+      stream_tok ((Tok.extract_string e) :: acc) str
+  in
+  let st = CLexer.get_lexer_state () in
+  try
+    let istr = Stream.of_string s in
+    let lex = CLexer.lexer.Plexing.tok_func istr in
+    let toks = stream_tok [] (fst lex) in
+    CLexer.set_lexer_state st;
+    toks
+  with exn ->
+    CLexer.set_lexer_state st;
+    raise (Diff_Failure "Input string is not lexable");;
+
+
+type hyp_info = {
+  idents: string list;
+  rhs_pp: Pp.t;
+  mutable done_: bool;
+}
+
+(* Generate the diffs between the old and new hyps.
+   This works by matching lines with the hypothesis name and diffing the right-hand side.
+   Lines that have multiple names such as "n, m : nat" are handled specially to account
+   for, say, the addition of m to a pre-existing "n : nat".
+ *)
+let diff_hyps o_line_idents o_map n_line_idents n_map =
+  let rv : Pp.t list ref = ref [] in
+
+  let is_done ident map = (StringMap.find ident map).done_ in
+  let exists ident map =
+    try let _ = StringMap.find ident map in true
+    with Not_found -> false in
+  let contains l ident = try [List.find (fun x  -> x = ident) l] with Not_found -> [] in
+
+  let output old_ids_uo new_ids =
+    (* 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
+
+    let setup ids map = if ids = [] then ("", Pp.mt ()) else
+      let open Pp in
+      let rhs_pp = (StringMap.find (List.hd ids) map).rhs_pp in
+      let pp_ids = List.map (fun x -> str x) ids in
+      let hyp_pp = List.fold_left (fun l1 l2 -> l1 ++ str ", " ++ l2) (List.hd pp_ids) (List.tl pp_ids) ++ rhs_pp in
+      (string_of_ppcmds hyp_pp, hyp_pp)
+    in
+
+    let (o_line, o_pp) = setup old_ids o_map in
+    let (n_line, n_pp) = setup new_ids n_map in
+
+    let hyp_diffs = diff_str ~tokenize_string o_line n_line in
+    let (has_added, has_removed) = has_changes hyp_diffs in
+    if show_removed () && has_removed then begin
+      let o_entry = StringMap.find (List.hd old_ids) o_map in
+      o_entry.done_ <- true;
+      rv := (add_diff_tags `Removed o_pp hyp_diffs) :: !rv;
+    end;
+    if n_line <> "" then begin
+      let n_entry = StringMap.find (List.hd new_ids) n_map in
+      n_entry.done_ <- true;
+      rv := (add_diff_tags `Added n_pp hyp_diffs) :: !rv
+    end
+  in
+
+  (* process identifier level diff *)
+  let process_ident_diff diff =
+    let (dtype, ident) = get_dinfo diff in
+    match dtype with
+    | `Removed ->
+      if dtype = `Removed then begin
+        let o_idents = (StringMap.find ident o_map).idents in
+        (* only show lines that have all idents removed here; other removed idents appear later *)
+        if show_removed () &&
+            List.for_all (fun x -> not (exists x n_map)) o_idents then
+          output (List.rev o_idents) []
+      end
+    | _ -> begin (* Added or Common case *)
+      let n_idents = (StringMap.find ident n_map).idents in
+
+      (* Process a new hyp line, possibly splitting it.  Duplicates some of
+         process_ident iteration, but easier to understand this way *)
+      let process_line ident2 =
+        if not (is_done ident2 n_map) then begin
+          let n_ids_list : string list ref = ref [] in
+          let o_ids_list : string list ref = ref [] in
+          let fst_omap_idents = ref None in
+          let add ids id map =
+            ids := id :: !ids;
+            (StringMap.find id map).done_ <- true in
+
+          (* get identifiers shared by one old and one new line, plus
+             other Added in new and other Removed in old *)
+          let process_split ident3 =
+            if not (is_done ident3 n_map) then begin
+              let this_omap_idents = try Some (StringMap.find ident3 o_map).idents
+                                    with Not_found -> None in
+              if !fst_omap_idents = None then
+                fst_omap_idents := this_omap_idents;
+              match (!fst_omap_idents, this_omap_idents) with
+              | (Some fst, Some this) when fst == this ->  (* yes, == *)
+                add n_ids_list ident3 n_map;
+                (* include, in old order, all undone Removed idents in old *)
+                List.iter (fun x -> if x = ident3 || not (is_done x o_map) && not (exists x n_map) then
+                                    (add o_ids_list x o_map)) fst
+              | (_, None) ->
+                add n_ids_list ident3 n_map (* include all undone Added idents in new *)
+              | _ -> ()
+            end in
+          List.iter process_split n_idents;
+          output (List.rev !o_ids_list) (List.rev !n_ids_list)
+        end in
+      List.iter process_line n_idents (* O(n^2), so sue me *)
+    end in
+
+  let cvt s = Array.of_list (List.concat s) in
+  let ident_diffs = diff_strs (cvt o_line_idents) (cvt n_line_idents) in
+  List.iter process_ident_diff ident_diffs;
+  List.rev !rv;;
+
+
+type 'a hyp = (Names.Id.t list * 'a option * 'a)
+type 'a reified_goal = { name: string; ty: 'a; hyps: 'a hyp list; env : Environ.env; sigma: Evd.evar_map }
+
+(* XXX: Port to proofview, one day. *)
+(* open Proofview *)
+module CDC = Context.Compacted.Declaration
+
+let to_tuple : Constr.compacted_declaration -> (Names.Id.t list * 'pc option * 'pc) =
+  let open CDC in function
+    | LocalAssum(idl, tm)   -> (idl, None, tm)
+    | LocalDef(idl,tdef,tm) -> (idl, Some tdef, tm);;
+
+(* XXX: Very unfortunately we cannot use the Proofview interface as
+   Proof is still using the "legacy" one. *)
+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
+  let ty   = Goal.V82.concl sigma g in
+  let name = Goal.uid g             in
+  (* There is a Constr/Econstr mess here... *)
+  let ty   = EConstr.to_constr sigma ty in
+  (* compaction is usually desired [eg for better display] *)
+  let hyps      = Termops.compact_named_context (Environ.named_context_of_val hyps) in
+  let hyps      = List.map to_tuple hyps in
+  { name; ty; hyps; env; sigma };;
+
+let pr_letype_core goal_concl_style env sigma t =
+  Ppconstr.pr_lconstr_expr (Constrextern.extern_type goal_concl_style env sigma t)
+
+let pp_of_type env sigma ty =
+  pr_letype_core true env sigma EConstr.(of_constr ty)
+
+(* 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:
+  b : bool
+  n, m : nat
+
+list will be [ ["b"]; ["n"; "m"] ]
+
+map will contain:
+  "b" -> { ["b"], Pp.t for ": bool"; false }
+  "n" -> { ["n"; "m"], Pp.t for ": nat"; false }
+  "m" -> { ["n"; "m"], Pp.t for ": nat"; false }
+ where the last two entries share the idents list.
+
+concl_pp is the conclusion as a Pp.t
+*)
+let goal_info goal sigma =
+  let map = ref StringMap.empty in
+  let line_idents = ref [] in
+  let build_hyp_info env sigma hyp =
+    let (names, body, ty) = hyp in
+    let open Pp in
+    let idents = List.map (fun x -> Names.Id.to_string x) names in
+
+    line_idents := idents :: !line_idents;
+    let mid = match body with
+    | Some x -> str " := " ++ pp_of_type env sigma ty ++ str " : "
+    | None -> str " : " in
+    let ts = pp_of_type env sigma ty in
+    let rhs_pp = mid ++ ts in
+
+    let make_entry () = { idents; rhs_pp; done_ = false } in
+    List.iter (fun ident -> map := (StringMap.add ident (make_entry ()) !map); ()) idents
+  in
+
+  try
+    let { ty=ty; hyps=hyps; env=env } = process_goal sigma goal in
+    List.iter (build_hyp_info env sigma) (List.rev hyps);
+    let concl_pp = pp_of_type env sigma ty in
+    ( List.rev !line_idents, !map, concl_pp )
+  with _ -> ([], !map, Pp.mt ());;
+
+let diff_goal_info o_info n_info =
+  let (o_line_idents, o_hyp_map, o_concl_pp) = o_info in
+  let (n_line_idents, n_hyp_map, n_concl_pp) = n_info in
+  let show_removed = Some (show_removed ()) in
+  let concl_pp = diff_pp_combined ~tokenize_string ?show_removed o_concl_pp n_concl_pp in
+
+  let hyp_diffs_list = diff_hyps o_line_idents o_hyp_map n_line_idents n_hyp_map in
+  (hyp_diffs_list, concl_pp)
+
+let hyp_list_to_pp hyps =
+  let open Pp in
+  match hyps with
+  | 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 open Pp in
+  v 0 (
+    (hyp_list_to_pp hyps_pp_list) ++ cut () ++
+    str "============================" ++ cut () ++
+    concl_pp);;
diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli
new file mode 100644
index 0000000000..0d3b5821e5
--- /dev/null
+++ b/printing/proof_diffs.mli
@@ -0,0 +1,67 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* diff options *)
+
+(** Controls whether to show diffs.  Takes values "on", "off", "removed" *)
+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.
+
+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
+raise Diff_Failure under some "impossible" conditions.
+
+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
+
+(** Computes the diff between two goals
+
+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
+raise Diff_Failure under some "impossible" conditions.
+
+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
+
+(** Convert a string to a list of token strings using the lexer *)
+val tokenize_string : string -> string list
+
+(* Exposed for unit test, don't use these otherwise *)
+(* output channel for the test log file *)
+val log_out_ch : out_channel ref
+
+
+type hyp_info = {
+  idents: string list;
+  rhs_pp: Pp.t;
+  mutable done_: bool;
+}
+
+module StringMap :
+sig
+  type +'a t
+  val empty: hyp_info t
+  val add : string -> hyp_info -> hyp_info t -> hyp_info t
+end
+
+val diff_hyps : string list list -> hyp_info StringMap.t -> string list list -> hyp_info StringMap.t -> Pp.t list
diff --git a/test-suite/unit-tests/clib/inteq.ml b/test-suite/unit-tests/clib/inteq.ml
index c07ec293f0..89717c79d5 100644
--- a/test-suite/unit-tests/clib/inteq.ml
+++ b/test-suite/unit-tests/clib/inteq.ml
@@ -1,5 +1,7 @@
 open Utest
 
+let log_out_ch = open_log_out_ch __FILE__
+
 let eq0 = mk_bool_test "clib-inteq0"
             "Int.equal on 0"
             (Int.equal 0 0)
@@ -10,4 +12,4 @@ let eq42 = mk_bool_test "clib-inteq42"
 
 let tests = [ eq0; eq42 ]
 
-let _ = run_tests __FILE__ tests
+let _ = run_tests __FILE__ log_out_ch tests
diff --git a/test-suite/unit-tests/clib/unicode_tests.ml b/test-suite/unit-tests/clib/unicode_tests.ml
index 9ae405977b..95316ad3aa 100644
--- a/test-suite/unit-tests/clib/unicode_tests.ml
+++ b/test-suite/unit-tests/clib/unicode_tests.ml
@@ -1,5 +1,7 @@
 open Utest
 
+let log_out_ch = open_log_out_ch __FILE__
+
 let unicode0 = mk_eq_test "clib-unicode0"
                  "split_at_first_letter, first letter is character"
                  None
@@ -12,4 +14,4 @@ let unicode1 = mk_eq_test "clib-unicode1"
 
 let tests = [ unicode0; unicode1 ]
 
-let _ = run_tests __FILE__ tests
+let _ = run_tests __FILE__ log_out_ch tests
diff --git a/test-suite/unit-tests/printing/proof_diffs_test.ml b/test-suite/unit-tests/printing/proof_diffs_test.ml
new file mode 100644
index 0000000000..526cefec44
--- /dev/null
+++ b/test-suite/unit-tests/printing/proof_diffs_test.ml
@@ -0,0 +1,333 @@
+open OUnit
+open Utest
+open Pp_diff
+open Proof_diffs
+
+let tokenize_string = Proof_diffs.tokenize_string
+let diff_pp = diff_pp ~tokenize_string
+let diff_str = diff_str ~tokenize_string
+
+let tests = ref []
+let add_test name test = tests := (mk_test name (TestCase test)) :: !tests
+
+let log_out_ch = open_log_out_ch __FILE__
+let cfprintf oc = Printf.(kfprintf (fun oc -> fprintf oc "") oc)
+let cprintf s = cfprintf log_out_ch s
+let _ = Proof_diffs.log_out_ch := log_out_ch
+
+let string_of_string s : string = "\"" ^ s ^ "\""
+
+(* todo: OCaml: why can't the body of the test function be given in the add_test line? *)
+
+let t () =
+  let expected : diff_list = [] in
+  let diffs = diff_str "" "   " in
+
+  assert_equal ~msg:"empty" ~printer:string_of_diffs expected diffs;
+  let (has_added, has_removed) = has_changes diffs in
+  assert_equal ~msg:"has `Added" ~printer:string_of_bool false has_added;
+  assert_equal ~msg:"has `Removed" ~printer:string_of_bool false has_removed
+let _ = add_test "diff_str empty" t
+
+
+let t () =
+  let expected : diff_list =
+    [ `Common (0, 0, "a"); `Common (1, 1, "b"); `Common (2, 2, "c")] in
+  let diffs = diff_str "a b c" " a  b\t  c\n" in
+
+  assert_equal ~msg:"white space" ~printer:string_of_diffs expected diffs;
+  let (has_added, has_removed) = has_changes diffs in
+  assert_equal ~msg:"no `Added" ~printer:string_of_bool false has_added;
+  assert_equal ~msg:"no `Removed" ~printer:string_of_bool false has_removed
+let _ = add_test "diff_str white space" t
+
+let t () =
+  let expected : diff_list = [ `Removed (0, "a"); `Added (0, "b")] in
+  let diffs = diff_str "a" "b" in
+
+  assert_equal ~msg:"add/remove" ~printer:string_of_diffs expected diffs;
+  let (has_added, has_removed) = has_changes diffs in
+  assert_equal ~msg:"has `Added" ~printer:string_of_bool true has_added;
+  assert_equal ~msg:"has `Removed" ~printer:string_of_bool true has_removed
+let _ = add_test "diff_str add/remove" t
+
+(* example of a limitation, not really a test *)
+let t () =
+  try
+    let _ = diff_str "a" "&gt;" in
+    assert_failure "unlexable string gives an exception"
+  with _ -> ()
+let _ = add_test "diff_str unlexable" t
+
+(* problematic examples for tokenize_string:
+   comments omitted
+   quoted string loses quote marks (are escapes supported/handled?)
+   char constant split into 2
+   *)
+let t () =
+  List.iter (fun x -> cprintf "'%s' " x) (tokenize_string "(* comment *) \"string\" 'c' xx");
+  cprintf "\n"
+let _ = add_test "tokenize_string examples" t
+
+open Pp
+
+(* note pp_to_string concatenates adjacent strings, could become one token,
+e.g. str " a" ++ str "b " will give a token "ab" *)
+(* checks background is present and correct *)
+let t () =
+  let o_pp = str "a" ++ str "!" ++ str "c" in
+  let n_pp = str "a" ++ str "?" ++ str "c" in
+  let (o_exp, n_exp) = (wrap_in_bg "diff.removed" (str "a" ++ (tag "diff.removed" (str "!")) ++ str "c"),
+                        wrap_in_bg "diff.added" (str "a" ++ (tag "diff.added" (str "?")) ++ str "c")) in
+  let (o_diff, n_diff) = diff_pp o_pp n_pp in
+
+  assert_equal ~msg:"removed" ~printer:db_string_of_pp o_exp o_diff;
+  assert_equal ~msg:"added"   ~printer:db_string_of_pp n_exp n_diff
+let _ = add_test "diff_pp/add_diff_tags add/remove" t
+
+let t () =
+  (*Printf.printf "%s\n" (string_of_diffs (diff_str "a d" "a b c d"));*)
+  let o_pp = str "a" ++ str " d" in
+  let n_pp = str "a" ++ str " b " ++ str " c " ++ str "d" ++ str " e " in
+  let n_exp = flatten (wrap_in_bg "diff.added" (seq [
+      str "a";
+      str " "; (tag "start.diff.added" (str "b "));
+      (tag "end.diff.added" (str " c")); str " ";
+      (str "d");
+      str " "; (tag "diff.added" (str "e")); str " "
+      ])) in
+  let (_, n_diff) = diff_pp o_pp n_pp in
+
+  assert_equal ~msg:"added"   ~printer:db_string_of_pp n_exp (flatten n_diff);;
+let _ = add_test "diff_pp/add_diff_tags a span with spaces" t
+
+
+let t () =
+  let o_pp = str " " in
+  let n_pp = tag "sometag" (str "a") in
+  let n_exp = flatten (wrap_in_bg "diff.added" (tag "diff.added" (tag "sometag" (str "a")))) in
+  let (_, n_diff) = diff_pp o_pp n_pp in
+
+  assert_equal ~msg:"added"   ~printer:db_string_of_pp n_exp (flatten n_diff)
+let _ = add_test "diff_pp/add_diff_tags diff tags outside existing tags" t
+
+let t () =
+  let o_pp = str " " in
+  let n_pp = seq [(tag "sometag" (str " a ")); str "b"] in
+  let n_exp = flatten (wrap_in_bg "diff.added"
+      (seq [tag "sometag" (str " "); (tag "start.diff.added" (tag "sometag" (str "a ")));
+          (tag "end.diff.added" (str "b"))]) ) in
+  let (_, n_diff) = diff_pp o_pp n_pp in
+
+  assert_equal ~msg:"added"   ~printer:db_string_of_pp n_exp (flatten n_diff)
+let _ = add_test "diff_pp/add_diff_tags existing tagged values with spaces" t
+
+let t () =
+  let o_pp = str " " in
+  let n_pp = str " a b " in
+  let n_exp = flatten (wrap_in_bg "diff.added"
+      (seq [str " "; tag "diff.added" (str "a b"); str " "])) in
+  let (_, n_diff) = diff_pp o_pp n_pp in
+
+  assert_equal ~msg:"added"   ~printer:db_string_of_pp n_exp (flatten n_diff)
+let _ = add_test "diff_pp/add_diff_tags multiple tokens in pp" t
+
+let t () =
+  let o_pp = str "a d" in
+  let n_pp = seq [str "a b"; str "c d"] in
+  let n_exp = flatten (wrap_in_bg "diff.added"
+      (seq [str "a "; tag "start.diff.added" (str "b");
+            tag "end.diff.added" (str "c"); str " d"])) in
+  let (_, n_diff) = diff_pp o_pp n_pp in
+
+  assert_equal ~msg:"added"   ~printer:db_string_of_pp n_exp (flatten n_diff)
+let _ = add_test "diff_pp/add_diff_tags token spanning multiple Ppcmd_strs" t
+
+let t () =
+  let o_pp = seq [str ""; str "a"] in
+  let n_pp = seq [str ""; str "a b"] in
+  let n_exp = flatten (wrap_in_bg "diff.added"
+      (seq [str ""; str "a "; tag "diff.added" (str "b")])) in
+  let (_, n_diff) = diff_pp o_pp n_pp in
+
+  assert_equal ~msg:"added"   ~printer:db_string_of_pp n_exp (flatten n_diff)
+let _ = add_test "diff_pp/add_diff_tags empty string preserved" t
+
+(* todo: awaiting a change in the lexer to return the quotes of the string token *)
+let t () =
+  let s = "\"a b\"" in
+  let o_pp = seq [str s] in
+  let n_pp = seq [str "\"a b\" "] in
+  cprintf "ppcmds: %s\n" (string_of_ppcmds n_pp);
+  let n_exp = flatten (wrap_in_bg "diff.added"
+      (seq [str ""; str "a "; tag "diff.added" (str "b")])) in
+  let (_, n_diff) = diff_pp o_pp n_pp in
+
+  assert_equal ~msg:"string" ~printer:string_of_string "a b" (List.hd (tokenize_string s));
+  assert_equal ~msg:"added"   ~printer:db_string_of_pp n_exp (flatten n_diff)
+let _ = if false then add_test "diff_pp/add_diff_tags token containing white space" t
+
+let add_entries map idents rhs_pp =
+  let make_entry() = { idents; rhs_pp; done_ = false } in
+  List.iter (fun ident -> map := (StringMap.add ident (make_entry ()) !map); ()) idents;;
+
+let print_list hyps = List.iter (fun x -> cprintf "%s\n" (string_of_ppcmds (flatten x))) hyps
+let db_print_list hyps = List.iter (fun x -> cprintf "%s\n" (db_string_of_pp (flatten x))) hyps
+
+
+(* a : foo
+   b : bar car ->
+   b : car
+   a : foo bar *)
+let t () =
+  write_diffs_option "removed";   (* turn on "removed" option *)
+  let o_line_idents = [ ["a"]; ["b"]] in
+  let o_hyp_map = ref StringMap.empty in
+  add_entries o_hyp_map ["a"] (str " : foo");
+  add_entries o_hyp_map ["b"] (str " : bar car");
+  let n_line_idents = [ ["b"]; ["a"]] in
+  let n_hyp_map = ref StringMap.empty in
+  add_entries n_hyp_map ["b"] (str " : car");
+  add_entries n_hyp_map ["a"] (str " : foo bar");
+  let expected = [flatten (wrap_in_bg "diff.removed" (seq [str "b"; str " : "; (tag "diff.removed" (str "bar")); str " car" ]));
+                  flatten (wrap_in_bg "diff.added" (seq [str "b"; str " : car" ]));
+                  flatten (wrap_in_bg "diff.added" (seq [str "a"; str " : foo "; (tag "diff.added" (str "bar")) ]))
+  ] in
+
+  let hyps_diff_list = diff_hyps o_line_idents !o_hyp_map n_line_idents !n_hyp_map in
+
+  (*print_list hyps_diff_list;*)
+  (*db_print_list hyps_diff_list;*)
+
+  List.iter2 (fun exp act ->
+      assert_equal ~msg:"added"   ~printer:db_string_of_pp exp (flatten act))
+      expected hyps_diff_list
+let _ = add_test "diff_hyps simple diffs" t
+
+(* a : nat
+  c, d : int ->
+  a, b : nat
+  d : int
+ and keeps old order *)
+let t () =
+  write_diffs_option "removed";   (* turn on "removed" option *)
+  let o_line_idents = [ ["a"]; ["c"; "d"]] in
+  let o_hyp_map = ref StringMap.empty in
+  add_entries o_hyp_map ["a"] (str " : nat");
+  add_entries o_hyp_map ["c"; "d"] (str " : int");
+  let n_line_idents = [ ["a"; "b"]; ["d"]] in
+  let n_hyp_map = ref StringMap.empty in
+  add_entries n_hyp_map ["a"; "b"] (str " : nat");
+  add_entries n_hyp_map ["d"] (str " : int");
+  let expected = [flatten (wrap_in_bg "diff.added" (seq [str "a"; (tag "start.diff.added" (str ", ")); (tag "end.diff.added" (str "b")); str " : nat" ]));
+                  flatten (wrap_in_bg "diff.removed" (seq [(tag "start.diff.removed" (str "c"));  (tag "end.diff.removed" (str ",")); str " "; str "d";  str " : int" ]));
+                  flatten (wrap_in_bg "diff.added" (seq [str "d"; str " : int" ]))
+  ] in
+
+  let hyps_diff_list = diff_hyps o_line_idents !o_hyp_map n_line_idents !n_hyp_map in
+
+  (*print_list hyps_diff_list;*)
+  (*print_list expected;*)
+
+  (*db_print_list hyps_diff_list;*)
+  (*db_print_list expected;*)
+
+  List.iter2 (fun exp act ->
+      assert_equal ~msg:"added"   ~printer:db_string_of_pp exp (flatten act))
+      expected hyps_diff_list
+let _ = add_test "diff_hyps compacted" t
+
+(* a : foo
+   b : bar
+   c : nat ->
+   b, a, c : nat
+DIFFS
+   b : bar (remove bar)
+   b : nat (add nat)
+   a : foo (remove foo)
+   a : nat (add nat)
+   c : nat
+ is this a realistic use case?
+*)
+let t () =
+  write_diffs_option "removed";   (* turn on "removed" option *)
+  let o_line_idents = [ ["a"]; ["b"]; ["c"]] in
+  let o_hyp_map = ref StringMap.empty in
+  add_entries o_hyp_map ["a"] (str " : foo");
+  add_entries o_hyp_map ["b"] (str " : bar");
+  add_entries o_hyp_map ["c"] (str " : nat");
+  let n_line_idents = [ ["b"; "a"; "c"] ] in
+  let n_hyp_map = ref StringMap.empty in
+  add_entries n_hyp_map ["b"; "a"; "c"] (str " : nat");
+  let expected = [flatten (wrap_in_bg "diff.removed" (seq [str "b"; str " : "; (tag "diff.removed" (str "bar"))]));
+                  flatten (wrap_in_bg "diff.added" (seq [str "b"; str " : "; (tag "diff.added" (str "nat"))]));
+                  flatten (wrap_in_bg "diff.removed" (seq [str "a"; str " : "; (tag "diff.removed" (str "foo"))]));
+                  flatten (wrap_in_bg "diff.added" (seq [str "a"; str " : "; (tag "diff.added" (str "nat"))]));
+                  flatten (seq [str "c"; str " : nat"])
+  ] in
+
+  let hyps_diff_list = diff_hyps o_line_idents !o_hyp_map n_line_idents !n_hyp_map in
+
+  (*print_list hyps_diff_list;*)
+  (*db_print_list hyps_diff_list;*)
+
+  List.iter2 (fun exp act ->
+      assert_equal ~msg:"added"   ~printer:db_string_of_pp exp (flatten act))
+      expected hyps_diff_list
+let _ = add_test "diff_hyps compacted with join" t
+
+(* b, a, c : nat ->
+   a : foo
+   b : bar
+   c : nat
+DIFFS
+   a : nat (remove nat)
+   a : foo (add foo)
+   b : nat (remove nat)
+   b : bar (add bar)
+   c : nat
+ is this a realistic use case? *)
+let t () =
+  write_diffs_option "removed";   (* turn on "removed" option *)
+  let o_line_idents = [ ["b"; "a"; "c"] ] in
+  let o_hyp_map = ref StringMap.empty in
+  add_entries o_hyp_map ["b"; "a"; "c"] (str " : nat");
+  let n_line_idents = [ ["a"]; ["b"]; ["c"]] in
+  let n_hyp_map = ref StringMap.empty in
+  add_entries n_hyp_map ["a"] (str " : foo");
+  add_entries n_hyp_map ["b"] (str " : bar");
+  add_entries n_hyp_map ["c"] (str " : nat");
+  let expected = [flatten (wrap_in_bg "diff.removed" (seq [str "a"; str " : "; (tag "diff.removed" (str "nat"))]));
+                  flatten (wrap_in_bg "diff.added" (seq [str "a"; str " : "; (tag "diff.added" (str "foo"))]));
+                  flatten (wrap_in_bg "diff.removed" (seq [str "b"; str " : "; (tag "diff.removed" (str "nat"))]));
+                  flatten (wrap_in_bg "diff.added" (seq [str "b"; str " : "; (tag "diff.added" (str "bar"))]));
+                  flatten (seq [str "c"; str " : nat"])
+  ] in
+
+  let hyps_diff_list = diff_hyps o_line_idents !o_hyp_map n_line_idents !n_hyp_map in
+
+  (*print_list hyps_diff_list;*)
+  (*db_print_list hyps_diff_list;*)
+
+  List.iter2 (fun exp act ->
+      assert_equal ~msg:"added"   ~printer:db_string_of_pp exp (flatten act))
+      expected hyps_diff_list
+let _ = add_test "diff_hyps compacted with split" t
+
+
+(* other potential tests
+coqtop/terminal formatting BLOCKED: CAN'T GET TAGS IN FORMATTER
+  white space at end of line
+  spanning diffs
+shorten_diff_span
+
+MAYBE NOT WORTH IT
+diff_pp/add_diff_tags
+  add/remove - show it preserves, recurs and processes:
+    nested in boxes
+    breaks, etc.  preserved
+diff_pp_combined with/without removed
+*)
+
+
+let _ = run_tests __FILE__ log_out_ch (List.rev !tests)
diff --git a/test-suite/unit-tests/src/utest.ml b/test-suite/unit-tests/src/utest.ml
index 069e6a4bf3..0cb1780ec9 100644
--- a/test-suite/unit-tests/src/utest.ml
+++ b/test-suite/unit-tests/src/utest.ml
@@ -42,10 +42,12 @@ let run_one logit test =
   let results = perform_test (fun _ -> ()) test in
   process_results results
 
-(* run list of OUnit test cases, log results *)
-let run_tests ml_fn tests =
+let open_log_out_ch ml_fn =
   let log_fn = ml_fn ^ ".log" in
-  let out_ch = open_out log_fn in
+  open_out log_fn
+
+(* run list of OUnit test cases, log results *)
+let run_tests ml_fn out_ch tests =
   let cprintf s = cfprintf out_ch s in
   let ceprintf s = cfprintf stderr s in
   let logit = logger out_ch in
diff --git a/test-suite/unit-tests/src/utest.mli b/test-suite/unit-tests/src/utest.mli
index 70928228bf..2e0f26e96b 100644
--- a/test-suite/unit-tests/src/utest.mli
+++ b/test-suite/unit-tests/src/utest.mli
@@ -9,4 +9,10 @@ val mk_bool_test : string -> string -> bool -> OUnit.test
 (* the string argument should be the name of the .ml file
    containing the tests; use __FILE__ for that purpose.
  *)
-val run_tests : string -> OUnit.test list -> unit
+val run_tests : string -> out_channel -> OUnit.test list -> unit
+
+(** open output channel for the test log file *)
+(* the string argument should be the name of the .ml file
+   containing the tests; use __FILE__ for that purpose.
+ *)
+val open_log_out_ch : string -> out_channel
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 89602c9b56..900964609d 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -68,6 +68,7 @@ type coq_cmdopts = {
   impredicative_set : Declarations.set_predicativity;
   stm_flags   : Stm.AsyncOpts.stm_opt;
   debug       : bool;
+  diffs_set   : bool;
   time        : bool;
 
   filter_opts : bool;
@@ -117,6 +118,7 @@ let init_args = {
   impredicative_set = Declarations.PredicativeSet;
   stm_flags    = Stm.AsyncOpts.default_opts;
   debug        = false;
+  diffs_set    = false;
   time         = false;
 
   filter_opts  = false;
@@ -526,6 +528,12 @@ let parse_args arglist : coq_cmdopts * string list =
     |"-color" -> set_color oval (next ())
     |"-config"|"--config" -> { oval with print_config = true }
     |"-debug" -> Coqinit.set_debug (); oval
+    |"-diffs" -> let opt = next () in
+                  if List.exists (fun x -> opt = x) ["off"; "on"; "removed"] then
+                    Proof_diffs.write_diffs_option opt
+                  else
+                    (prerr_endline ("Error: on|off|removed expected after -diffs"); exit 1);
+                  { oval with diffs_set = true }
     |"-stm-debug" -> Stm.stm_debug := true; oval
     |"-emacs" -> set_emacs oval
     |"-filteropts" -> { oval with filter_opts = true }
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index 9fb6219a61..7b0cdcf127 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -43,6 +43,7 @@ type coq_cmdopts = {
   impredicative_set : Declarations.set_predicativity;
   stm_flags   : Stm.AsyncOpts.stm_opt;
   debug       : bool;
+  diffs_set   : bool;
   time        : bool;
 
   filter_opts : bool;
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 7ae15ac100..7b7e1b16c0 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -318,12 +318,6 @@ let loop_flush_all () =
   Format.pp_print_flush !Topfmt.std_ft ();
   Format.pp_print_flush !Topfmt.err_ft ()
 
-let pr_open_cur_subgoals () =
-  try
-    let proof = Proof_global.give_me_the_proof () in
-    Printer.pr_open_subgoals ~proof
-  with Proof_global.NoCurrentProof -> Pp.str ""
-
 (* Goal equality heuristic. *)
 let pequal cmp1 cmp2 (a1,a2) (b1,b2) = cmp1 a1 b1 && cmp2 a2 b2
 let evleq e1 e2 = CList.equal Evar.equal e1 e2
@@ -346,7 +340,7 @@ let top_goal_print oldp newp =
     let proof_changed = not (Option.equal cproof oldp newp) in
     let print_goals = not !Flags.quiet &&
                       proof_changed && Proof_global.there_are_pending_proofs () in
-    if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ())
+    if print_goals then Printer.print_and_diff oldp newp;
   with
   | exn ->
     let (e, info) = CErrors.push exn in
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index e979d0e544..9b68f303a6 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -339,8 +339,8 @@ let do_vio opts =
 (******************************************************************************)
 (* Color Options                                                              *)
 (******************************************************************************)
-let init_color color_mode =
-  let has_color = match color_mode with
+let init_color opts =
+  let has_color = match opts.color with
   | `OFF -> false
   | `ON -> true
   | `AUTO ->
@@ -350,26 +350,23 @@ let init_color color_mode =
        its TERM variable is set to "dumb". *)
     try Sys.getenv "TERM" <> "dumb" with Not_found -> false
   in
-  if has_color then begin
-    let colors = try Some (Sys.getenv "COQ_COLORS") with Not_found -> None in
-    match colors with
-    | None ->
-      (** Default colors *)
-      Topfmt.default_styles ();
-      Topfmt.init_terminal_output ~color:true
-    | Some "" ->
-      (** No color output *)
-      Topfmt.init_terminal_output ~color:false
-    | Some s ->
-      (** Overwrite all colors *)
-      Topfmt.parse_color_config s;
-      Topfmt.init_terminal_output ~color:true
-  end
-  else
-    Topfmt.init_terminal_output ~color:false
+  let term_color =
+    if has_color then begin
+      let colors = try Some (Sys.getenv "COQ_COLORS") with Not_found -> None in
+      match colors with
+      | None -> Topfmt.default_styles (); true        (** Default colors *)
+      | Some "" -> false                              (** No color output *)
+      | Some s -> Topfmt.parse_color_config s; true   (** Overwrite all colors *)
+    end
+    else
+      false
+  in
+  if Proof_diffs.show_diffs () && not term_color && not opts.batch_mode then
+    CErrors.user_err Pp.(str "Error: -diffs requires enabling -color");
+  Topfmt.init_terminal_output ~color:term_color
 
 let print_style_tags opts =
-  let () = init_color opts.color in
+  let () = init_color opts in
   let tags = Topfmt.dump_tags () in
   let iter (t, st) =
     let opt = Terminal.eval st ^ t ^ Terminal.reset ^ "\n" in
@@ -520,7 +517,7 @@ type custom_toplevel = {
 }
 
 let coqtop_init ~opts extra =
-  init_color opts.color;
+  init_color opts;
   CoqworkmgrApi.(init !async_proofs_worker_priority);
   opts, extra
 
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 504ffa521b..d85fed5f43 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -72,7 +72,8 @@ let print_usage_channel co command =
 \n  -boot                  boot mode (implies -q and -batch)\
 \n  -bt                    print backtraces (requires configure debug flag)\
 \n  -debug                 debug mode (implies -bt)\
-\n  -stm-debug             STM debug mode (will trace every transaction) \
+\n  -diffs (on|off|removed) highlight differences between proof steps\
+\n  -stm-debug             STM debug mode (will trace every transaction)\
 \n  -emacs                 tells Coq it is executed under Emacs\
 \n  -noglob                do not dump globalizations\
 \n  -dump-glob f           dump globalizations in file f (to be used by coqdoc)\
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index 609dac69aa..f842ca5ead 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -181,6 +181,10 @@ let default_tag_map () = let open Terminal in [
   ; "tactic.keyword"   , make ~bold:true ()
   ; "tactic.primitive" , make ~fg_color:`LIGHT_GREEN ()
   ; "tactic.string"    , make ~fg_color:`LIGHT_RED ()
+  ; "diff.added"       , make ~bg_color:(`RGB(0,141,0)) ~underline:true ()
+  ; "diff.removed"     , make ~bg_color:(`RGB(170,0,0)) ~underline:true ()
+  ; "diff.added.bg"    , make ~bg_color:(`RGB(0,91,0)) ()
+  ; "diff.removed.bg"  , make ~bg_color:(`RGB(91,0,0)) ()
   ]
 
 let tag_map = ref CString.Map.empty
@@ -198,72 +202,103 @@ let parse_color_config file =
 
 let dump_tags () = CString.Map.bindings !tag_map
 
+let empty = Terminal.make ()
+let default_style = Terminal.reset_style
+
+let get_style tag =
+  try CString.Map.find tag !tag_map
+  with Not_found -> empty;;
+
+let get_open_seq tags =
+  let style = List.fold_left (fun a b -> Terminal.merge a (get_style b)) default_style tags in
+  Terminal.eval (Terminal.diff default_style style);;
+
+let get_close_seq tags =
+  let style = List.fold_left (fun a b -> Terminal.merge a (get_style b)) default_style tags in
+  Terminal.eval (Terminal.diff style default_style);;
+
+let diff_tag_stack = ref []  (* global, just like std_ft *)
+
 (** Not thread-safe. We should put a lock somewhere if we print from
     different threads. Do we? *)
 let make_style_stack () =
   (** Default tag is to reset everything *)
-  let empty = Terminal.make () in
-  let default_tag = Terminal.({
-      fg_color = Some `DEFAULT;
-      bg_color = Some `DEFAULT;
-      bold = Some false;
-      italic = Some false;
-      underline = Some false;
-      negative = Some false;
-      prefix = None;
-      suffix = None;
-    })
-  in
   let style_stack = ref [] in
   let peek () = match !style_stack with
-  | []      -> default_tag  (** Anomalous case, but for robustness *)
+  | []      -> default_style  (** Anomalous case, but for robustness *)
   | st :: _ -> st
   in
-  let push tag =
-    let style =
-      try CString.Map.find tag !tag_map
-      with | Not_found -> empty
-    in
-    (** Use the merging of the latest tag and the one being currently pushed.
-    This may be useful if for instance the latest tag changes the background and
-    the current one the foreground, so that the two effects are additioned. *)
+  let open_tag tag =
+    let (tpfx, ttag) = split_tag tag in
+    if tpfx = end_pfx then "" else
+      let style = get_style ttag in
+    (** Merge the current settings and the style being pushed.  This allows
+    restoring the previous settings correctly in a pop when both set the same
+    attribute.  Example: current settings have red FG, the pushed style has
+    green FG.  When popping the style, we should set red FG, not default FG. *)
     let style = Terminal.merge (peek ()) style in
+    let diff = Terminal.diff (peek ()) style in
     style_stack := style :: !style_stack;
-    Terminal.eval style
+    if tpfx = start_pfx then diff_tag_stack := ttag :: !diff_tag_stack;
+    Terminal.eval diff
   in
-  let pop _ = match !style_stack with
-  | []       -> (** Something went wrong, we fallback *)
-                Terminal.eval default_tag
-  | _ :: rem -> style_stack := rem;
-                Terminal.eval (peek ())
+  let close_tag tag =
+    let (tpfx, _) = split_tag tag in
+      if tpfx = start_pfx then "" else begin
+        if tpfx = end_pfx then diff_tag_stack := (try List.tl !diff_tag_stack with tl -> []);
+        match !style_stack with
+        | []       -> (** Something went wrong, we fallback *)
+                      Terminal.eval default_style
+        | cur :: rem -> style_stack := rem;
+                      if cur = (peek ()) then "" else
+                        if rem = [] then Terminal.reset else
+                          Terminal.eval (Terminal.diff cur (peek ()))
+      end
   in
   let clear () = style_stack := [] in
-  push, pop, clear
+  open_tag, close_tag, clear
 
 let make_printing_functions () =
-  let empty = Terminal.make () in
   let print_prefix ft tag =
-    let style =
-      try CString.Map.find tag !tag_map
-      with | Not_found -> empty
-    in
-    match style.Terminal.prefix with Some s -> Format.pp_print_string ft s | None -> ()
-  in
+    let (tpfx, ttag) = split_tag tag in
+    if tpfx <> end_pfx then
+      let style = get_style ttag in
+      match style.Terminal.prefix with Some s -> Format.pp_print_string ft s | None -> () in
+
   let print_suffix ft tag =
-    let style =
-      try CString.Map.find tag !tag_map
-      with | Not_found -> empty
-    in
-    match style.Terminal.suffix with Some s -> Format.pp_print_string ft s | None -> ()
-  in
+    let (tpfx, ttag) = split_tag tag in
+    if tpfx <> start_pfx then
+      let style = get_style ttag in
+      match style.Terminal.suffix with Some s -> Format.pp_print_string ft s | None -> () in
+
   print_prefix, print_suffix
 
+let init_output_fns () =
+  let reopen_highlight = ref "" in
+  let open Format in
+  let fns = Format.pp_get_formatter_out_functions !std_ft () in
+  let newline () =
+    if !diff_tag_stack <> [] then begin
+      let close = get_close_seq !diff_tag_stack in
+      fns.out_string close 0 (String.length close);
+      reopen_highlight := get_open_seq (List.rev !diff_tag_stack);
+    end;
+    fns.out_string "\n" 0 1 in
+  let string s off n =
+    if !reopen_highlight <> ""  && String.trim (String.sub s off n) <> "" then begin
+      fns.out_string !reopen_highlight 0 (String.length !reopen_highlight);
+      reopen_highlight := ""
+    end;
+    fns.out_string s off n in
+  let new_fns = { fns with out_string = string; out_newline = newline } in
+  Format.pp_set_formatter_out_functions !std_ft new_fns;;
+
 let init_terminal_output ~color =
-  let push_tag, pop_tag, clear_tag = make_style_stack () in
+  let open_tag, close_tag, clear_tag = make_style_stack () in
   let print_prefix, print_suffix = make_printing_functions () in
   let tag_handler ft = {
-    Format.mark_open_tag   = push_tag;
-    Format.mark_close_tag  = pop_tag;
+    Format.mark_open_tag   = open_tag;
+    Format.mark_close_tag  = close_tag;
     Format.print_open_tag  = print_prefix ft;
     Format.print_close_tag = print_suffix ft;
   } in
@@ -271,6 +306,7 @@ let init_terminal_output ~color =
     (* Use 0-length markers *)
     begin
       std_logger_cleanup := clear_tag;
+      init_output_fns ();
       Format.pp_set_mark_tags !std_ft true;
       Format.pp_set_mark_tags !err_ft true
     end