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.

Diffs are computed for the hypotheses and conclusion of the first goal between
the old and new proofs. Strings are split into tokens using the Coq lexer,
then the list of tokens are diffed using the Myers algorithm.  A fixup routine
(Pp_diff.shorten_diff_span) shortens the span of the diff result in some cases.

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.

The 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.

25 files changed, 1792 insertions, 95 deletions

diff --git a/CHANGES b/CHANGES
index d3f07889fe..ea4ced4d9b 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
@@ -105,12 +105,20 @@ 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
   rewriting and then discarded).
 
+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/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..8633609be8
--- /dev/null
+++ b/lib/pp_diff.ml
@@ -0,0 +1,296 @@
+(************************************************************************)
+(*         *   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);;
+
+(* to be set to Proof_diffs.tokenize_string to allow a forward reference to the lexer *)
+let tokenize_string = ref (fun (s : string) -> [s])
+
+(* get the Myers diff of 2 strings *)
+let diff_str 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 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 o_str n_str in
+  (add_diff_tags `Removed o_pp diffs, add_diff_tags `Added n_pp diffs);;
+
+let diff_pp_combined ?(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 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..94b00fed6a
--- /dev/null
+++ b/lib/pp_diff.mli
@@ -0,0 +1,119 @@
+(************************************************************************)
+(*         *   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 : 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 : ?show_removed:bool -> Pp.t -> Pp.t -> Pp.t
+
+(** Raised if the diff fails *)
+exception Diff_Failure of string
+
+(* for dependency injection to allow calling the lexer *)
+val tokenize_string : (string -> string list) ref
+
+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 : 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..5043759d32
--- /dev/null
+++ b/printing/proof_diffs.ml
@@ -0,0 +1,342 @@
+(************************************************************************)
+(*         *   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);;
+
+(* placed here so that pp_diff.ml can access the lexer through dependency injection *)
+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");;
+
+let _ = Pp_diff.tokenize_string := tokenize_string
+
+
+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 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..481b664d8a
--- /dev/null
+++ b/printing/proof_diffs.mli
@@ -0,0 +1,64 @@
+(************************************************************************)
+(*         *   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
+
+(* 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/printing/proof_diffs_test.ml b/test-suite/unit-tests/printing/proof_diffs_test.ml
new file mode 100644
index 0000000000..e0285ac143
--- /dev/null
+++ b/test-suite/unit-tests/printing/proof_diffs_test.ml
@@ -0,0 +1,331 @@
+open OUnit
+open Utest
+open Pp_diff
+open Proof_diffs
+
+let tokenize_string = !Pp_diff.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/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 ecf9733041..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,22 +202,36 @@ 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.reset_style 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
+  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
@@ -221,43 +239,66 @@ let make_style_stack () =
     let style = Terminal.merge (peek ()) style in
     let diff = Terminal.diff (peek ()) style in
     style_stack := style :: !style_stack;
+    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
-  | cur :: rem -> style_stack := rem;
-                if cur = (peek ()) then "" else
-                  if List.length rem = 0 then Terminal.reset else
-                    Terminal.eval (Terminal.diff cur (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
@@ -265,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