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.

5 files changed, 491 insertions, 22 deletions

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