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

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..7131ced15b
--- /dev/null
+++ b/printing/proof_diffs.ml
@@ -0,0 +1,339 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(*
+Displays the differences between successive proof steps in coqtop and CoqIDE.
+Proof General requires minor changes to make the diffs visible, but this code
+shouldn't break the existing version of PG.  See pp_diff.ml for details on how
+the diff works.
+
+Diffs are computed for the hypotheses and conclusion of the first goal between
+the old and new proofs.
+
+Diffs can be enabled with the Coq commmand "Set Diffs on|off|removed." or
+'-diffs "on"|"off"|"removed"' on the OS command line.  The "on" option shows only the
+new item with added text, while "removed" shows each modified item twice--once
+with the old value showing removed text and once with the new value showing
+added text.
+
+In CoqIDE, colors and highlights can be set in the Edit/Preferences/Tags panel.
+For coqtop, these can be set through the COQ_COLORS environment variable.
+
+Limitations/Possible enhancements:
+
+- If you go back to a prior proof step, diffs are not shown on the new current
+step.  Diffs will be shown again once you do another proof step.
+
+- Diffs are done between the first active goal in the old and new proofs.
+If, for example, the proof step completed a goal, then the new goal is a
+different goal, not a transformation of the old goal, so a diff is probably
+not appropriate.  (There's currently no way to tell when this happens or to
+accurately match goals across old and new proofs.
+See https://github.com/coq/coq/issues/7653)  This is also why only the
+first goal is diffed.
+
+- "Set Diffs "xx"." should reprint the current goal using the new option.
+
+- coqtop colors were chosen for white text on a black background.  They're
+not the greatest.  I didn't want to change the existing green highlight.
+Suggestions welcome.
+
+- coqtop underlines removed text because (per Wikipedia) the ANSI escape code
+for strikeout is not commonly supported (it didn't work on mine).  CoqIDE
+uses strikeout on removed text.
+*)
+
+open Pp_diff
+
+let diff_option = ref `OFF
+
+(* todo: Is there a way to persist the setting between sessions?
+   Eg if the user wants this as a permanent config setting? *)
+let read_diffs_option () = match !diff_option with
+| `OFF -> "off"
+| `ON -> "on"
+| `REMOVED -> "removed"
+
+let write_diffs_option = function
+| "off" -> diff_option := `OFF
+| "on" -> diff_option := `ON
+| "removed" -> diff_option := `REMOVED
+| _ -> CErrors.user_err Pp.(str "Diffs option only accepts the following values: \"off\", \"on\", \"removed\".")
+
+let _ =
+  Goptions.(declare_string_option {
+    optdepr = false;
+    optname = "show diffs in proofs";
+    optkey = ["Diffs"];
+    optread = read_diffs_option;
+    optwrite = write_diffs_option
+  })
+
+let show_diffs () = !diff_option <> `OFF;;
+let show_removed () = !diff_option = `REMOVED;;
+
+
+(* DEBUG/UNIT TEST *)
+let cfprintf oc = Printf.(kfprintf (fun oc -> fprintf oc "") oc)
+let log_out_ch = ref stdout
+[@@@ocaml.warning "-32"]
+let cprintf s = cfprintf !log_out_ch s
+[@@@ocaml.warning "+32"]
+
+module StringMap = Map.Make(String);;
+
+let tokenize_string s =
+  (* todo: cLexer changes buff as it proceeds.  Seems like that should be saved, too.
+  But I don't understand how it's used--it looks like things get appended to it but
+  it never gets cleared. *)
+  let rec stream_tok acc str =
+    let e = Stream.next str in
+    if Tok.(equal e EOI) then
+      List.rev acc
+    else
+      stream_tok ((Tok.extract_string e) :: acc) str
+  in
+  let st = CLexer.get_lexer_state () in
+  try
+    let istr = Stream.of_string s in
+    let lex = CLexer.lexer.Plexing.tok_func istr in
+    let toks = stream_tok [] (fst lex) in
+    CLexer.set_lexer_state st;
+    toks
+  with exn ->
+    CLexer.set_lexer_state st;
+    raise (Diff_Failure "Input string is not lexable");;
+
+
+type hyp_info = {
+  idents: string list;
+  rhs_pp: Pp.t;
+  mutable done_: bool;
+}
+
+(* Generate the diffs between the old and new hyps.
+   This works by matching lines with the hypothesis name and diffing the right-hand side.
+   Lines that have multiple names such as "n, m : nat" are handled specially to account
+   for, say, the addition of m to a pre-existing "n : nat".
+ *)
+let diff_hyps o_line_idents o_map n_line_idents n_map =
+  let rv : Pp.t list ref = ref [] in
+
+  let is_done ident map = (StringMap.find ident map).done_ in
+  let exists ident map =
+    try let _ = StringMap.find ident map in true
+    with Not_found -> false in
+  let contains l ident = try [List.find (fun x  -> x = ident) l] with Not_found -> [] in
+
+  let output old_ids_uo new_ids =
+    (* use the order from the old line in case it's changed in the new *)
+    let old_ids = if old_ids_uo = [] then [] else
+      let orig = (StringMap.find (List.hd old_ids_uo) o_map).idents in
+      List.concat (List.map (contains orig) old_ids_uo) in
+
+    let setup ids map = if ids = [] then ("", Pp.mt ()) else
+      let open Pp in
+      let rhs_pp = (StringMap.find (List.hd ids) map).rhs_pp in
+      let pp_ids = List.map (fun x -> str x) ids in
+      let hyp_pp = List.fold_left (fun l1 l2 -> l1 ++ str ", " ++ l2) (List.hd pp_ids) (List.tl pp_ids) ++ rhs_pp in
+      (string_of_ppcmds hyp_pp, hyp_pp)
+    in
+
+    let (o_line, o_pp) = setup old_ids o_map in
+    let (n_line, n_pp) = setup new_ids n_map in
+
+    let hyp_diffs = diff_str ~tokenize_string o_line n_line in
+    let (has_added, has_removed) = has_changes hyp_diffs in
+    if show_removed () && has_removed then begin
+      let o_entry = StringMap.find (List.hd old_ids) o_map in
+      o_entry.done_ <- true;
+      rv := (add_diff_tags `Removed o_pp hyp_diffs) :: !rv;
+    end;
+    if n_line <> "" then begin
+      let n_entry = StringMap.find (List.hd new_ids) n_map in
+      n_entry.done_ <- true;
+      rv := (add_diff_tags `Added n_pp hyp_diffs) :: !rv
+    end
+  in
+
+  (* process identifier level diff *)
+  let process_ident_diff diff =
+    let (dtype, ident) = get_dinfo diff in
+    match dtype with
+    | `Removed ->
+      if dtype = `Removed then begin
+        let o_idents = (StringMap.find ident o_map).idents in
+        (* only show lines that have all idents removed here; other removed idents appear later *)
+        if show_removed () &&
+            List.for_all (fun x -> not (exists x n_map)) o_idents then
+          output (List.rev o_idents) []
+      end
+    | _ -> begin (* Added or Common case *)
+      let n_idents = (StringMap.find ident n_map).idents in
+
+      (* Process a new hyp line, possibly splitting it.  Duplicates some of
+         process_ident iteration, but easier to understand this way *)
+      let process_line ident2 =
+        if not (is_done ident2 n_map) then begin
+          let n_ids_list : string list ref = ref [] in
+          let o_ids_list : string list ref = ref [] in
+          let fst_omap_idents = ref None in
+          let add ids id map =
+            ids := id :: !ids;
+            (StringMap.find id map).done_ <- true in
+
+          (* get identifiers shared by one old and one new line, plus
+             other Added in new and other Removed in old *)
+          let process_split ident3 =
+            if not (is_done ident3 n_map) then begin
+              let this_omap_idents = try Some (StringMap.find ident3 o_map).idents
+                                    with Not_found -> None in
+              if !fst_omap_idents = None then
+                fst_omap_idents := this_omap_idents;
+              match (!fst_omap_idents, this_omap_idents) with
+              | (Some fst, Some this) when fst == this ->  (* yes, == *)
+                add n_ids_list ident3 n_map;
+                (* include, in old order, all undone Removed idents in old *)
+                List.iter (fun x -> if x = ident3 || not (is_done x o_map) && not (exists x n_map) then
+                                    (add o_ids_list x o_map)) fst
+              | (_, None) ->
+                add n_ids_list ident3 n_map (* include all undone Added idents in new *)
+              | _ -> ()
+            end in
+          List.iter process_split n_idents;
+          output (List.rev !o_ids_list) (List.rev !n_ids_list)
+        end in
+      List.iter process_line n_idents (* O(n^2), so sue me *)
+    end in
+
+  let cvt s = Array.of_list (List.concat s) in
+  let ident_diffs = diff_strs (cvt o_line_idents) (cvt n_line_idents) in
+  List.iter process_ident_diff ident_diffs;
+  List.rev !rv;;
+
+
+type 'a hyp = (Names.Id.t list * 'a option * 'a)
+type 'a reified_goal = { name: string; ty: 'a; hyps: 'a hyp list; env : Environ.env; sigma: Evd.evar_map }
+
+(* XXX: Port to proofview, one day. *)
+(* open Proofview *)
+module CDC = Context.Compacted.Declaration
+
+let to_tuple : Constr.compacted_declaration -> (Names.Id.t list * 'pc option * 'pc) =
+  let open CDC in function
+    | LocalAssum(idl, tm)   -> (idl, None, tm)
+    | LocalDef(idl,tdef,tm) -> (idl, Some tdef, tm);;
+
+(* XXX: Very unfortunately we cannot use the Proofview interface as
+   Proof is still using the "legacy" one. *)
+let process_goal sigma g : Constr.t reified_goal =
+  let env  = Goal.V82.env   sigma g in
+  let hyps = Goal.V82.hyps  sigma g in
+  let ty   = Goal.V82.concl sigma g in
+  let name = Goal.uid g             in
+  (* There is a Constr/Econstr mess here... *)
+  let ty   = EConstr.to_constr sigma ty in
+  (* compaction is usually desired [eg for better display] *)
+  let hyps      = Termops.compact_named_context (Environ.named_context_of_val hyps) in
+  let hyps      = List.map to_tuple hyps in
+  { name; ty; hyps; env; sigma };;
+
+let pr_letype_core goal_concl_style env sigma t =
+  Ppconstr.pr_lconstr_expr (Constrextern.extern_type goal_concl_style env sigma t)
+
+let pp_of_type env sigma ty =
+  pr_letype_core true env sigma EConstr.(of_constr ty)
+
+(* fetch info from a goal, returning (idents, map, concl_pp) where
+idents is a list with one entry for each hypothesis, each entry is the list of
+idents on the lhs of the hypothesis.  map is a map from ident to hyp_info
+reoords.  For example: for the hypotheses:
+  b : bool
+  n, m : nat
+
+list will be [ ["b"]; ["n"; "m"] ]
+
+map will contain:
+  "b" -> { ["b"], Pp.t for ": bool"; false }
+  "n" -> { ["n"; "m"], Pp.t for ": nat"; false }
+  "m" -> { ["n"; "m"], Pp.t for ": nat"; false }
+ where the last two entries share the idents list.
+
+concl_pp is the conclusion as a Pp.t
+*)
+let goal_info goal sigma =
+  let map = ref StringMap.empty in
+  let line_idents = ref [] in
+  let build_hyp_info env sigma hyp =
+    let (names, body, ty) = hyp in
+    let open Pp in
+    let idents = List.map (fun x -> Names.Id.to_string x) names in
+
+    line_idents := idents :: !line_idents;
+    let mid = match body with
+    | Some x -> str " := " ++ pp_of_type env sigma ty ++ str " : "
+    | None -> str " : " in
+    let ts = pp_of_type env sigma ty in
+    let rhs_pp = mid ++ ts in
+
+    let make_entry () = { idents; rhs_pp; done_ = false } in
+    List.iter (fun ident -> map := (StringMap.add ident (make_entry ()) !map); ()) idents
+  in
+
+  try
+    let { ty=ty; hyps=hyps; env=env } = process_goal sigma goal in
+    List.iter (build_hyp_info env sigma) (List.rev hyps);
+    let concl_pp = pp_of_type env sigma ty in
+    ( List.rev !line_idents, !map, concl_pp )
+  with _ -> ([], !map, Pp.mt ());;
+
+let diff_goal_info o_info n_info =
+  let (o_line_idents, o_hyp_map, o_concl_pp) = o_info in
+  let (n_line_idents, n_hyp_map, n_concl_pp) = n_info in
+  let show_removed = Some (show_removed ()) in
+  let concl_pp = diff_pp_combined ~tokenize_string ?show_removed o_concl_pp n_concl_pp in
+
+  let hyp_diffs_list = diff_hyps o_line_idents o_hyp_map n_line_idents n_hyp_map in
+  (hyp_diffs_list, concl_pp)
+
+let hyp_list_to_pp hyps =
+  let open Pp in
+  match hyps with
+  | h :: tl -> List.fold_left (fun x y -> x ++ cut () ++ y) h tl
+  | [] -> mt ();;
+
+(* Special purpuse, use only for the IDE interface,  *)
+let diff_first_goal o_proof n_proof =
+  let first_goal_info proof =
+    match proof with
+    | None -> ([], StringMap.empty, Pp.mt ())
+    | Some proof2 ->
+      let (goals,_,_,_,sigma) = Proof.proof proof2 in
+      match goals with
+      | hd :: tl -> goal_info hd sigma;
+      | _ -> ([], StringMap.empty, Pp.mt ())
+  in
+  diff_goal_info (first_goal_info o_proof) (first_goal_info n_proof);;
+
+let diff_goals ?prev_gs n_gs =
+  let unwrap gs =
+    match gs with
+    | Some gs ->
+      let goal = Evd.sig_it gs in
+      let sigma = Refiner.project gs in
+      goal_info goal sigma
+    | None -> ([], StringMap.empty, Pp.mt ())
+  in
+  let (hyps_pp_list, concl_pp) = diff_goal_info (unwrap prev_gs) (unwrap n_gs) in
+  let open Pp in
+  v 0 (
+    (hyp_list_to_pp hyps_pp_list) ++ cut () ++
+    str "============================" ++ cut () ++
+    concl_pp);;
diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli
new file mode 100644
index 0000000000..0d3b5821e5
--- /dev/null
+++ b/printing/proof_diffs.mli
@@ -0,0 +1,67 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* diff options *)
+
+(** Controls whether to show diffs.  Takes values "on", "off", "removed" *)
+val write_diffs_option : string -> unit
+(** Returns true if the diffs option is "on" or "removed" *)
+val show_diffs : unit -> bool
+
+(** Computes the diff between the first goal of two Proofs and returns
+the highlighted hypotheses and conclusion.
+
+If the strings used to display the goal are not lexable (this is believed
+unlikely), this routine will generate a Diff_Failure.  This routine may also
+raise Diff_Failure under some "impossible" conditions.
+
+If you want to make your call especially bulletproof, catch these
+exceptions, print a user-visible message, then recall this routine with
+the first argument set to None, which will skip the diff.
+*)
+val diff_first_goal : Proof.t option -> Proof.t option -> Pp.t list * Pp.t
+
+open Evd
+open Proof_type
+
+(** Computes the diff between two goals
+
+If the strings used to display the goal are not lexable (this is believed
+unlikely), this routine will generate a Diff_Failure.  This routine may also
+raise Diff_Failure under some "impossible" conditions.
+
+If you want to make your call especially bulletproof, catch these
+exceptions, print a user-visible message, then recall this routine with
+the first argument set to None, which will skip the diff.
+*)
+val diff_goals : ?prev_gs:(goal sigma) -> goal sigma option -> Pp.t
+
+(** Convert a string to a list of token strings using the lexer *)
+val tokenize_string : string -> string list
+
+(* Exposed for unit test, don't use these otherwise *)
+(* output channel for the test log file *)
+val log_out_ch : out_channel ref
+
+
+type hyp_info = {
+  idents: string list;
+  rhs_pp: Pp.t;
+  mutable done_: bool;
+}
+
+module StringMap :
+sig
+  type +'a t
+  val empty: hyp_info t
+  val add : string -> hyp_info -> hyp_info t -> hyp_info t
+end
+
+val diff_hyps : string list list -> hyp_info StringMap.t -> string list list -> hyp_info StringMap.t -> Pp.t list