9 files changed, 120 insertions, 16 deletions

diff --git a/CHANGES.md b/CHANGES.md
index af2b7991dd..90ededb8f3 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -219,6 +219,12 @@ SSReflect
   - `=> {x..} /H`      ->  `=> /v {x..H}`
   - `rewrite {x..} H`  ->  `rewrite E {x..H}`
 
+Diffs
+
+- Some error messages that show problems with a pair of non-matching values will now
+  highlight the differences.
+
+
 Changes from 8.8.2 to 8.9+beta1
 ===============================
 
diff --git a/doc/sphinx/_static/diffs-error-message.png b/doc/sphinx/_static/diffs-error-message.png
new file mode 100644
index 0000000000..6733d9c6a9
--- /dev/null
+++ b/doc/sphinx/_static/diffs-error-message.png
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 2300a317f1..d0bd9e396d 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -628,7 +628,8 @@ Showing differences between proof steps
 ---------------------------------------
 
 
-Coq can automatically highlight the differences between successive proof steps.
+Coq can automatically highlight the differences between successive proof steps and between
+values in some error messages.
 For example, the following screenshots of CoqIDE and coqtop show the application
 of the same :tacn:`intros` tactic.  The tactic creates two new hypotheses, highlighted in green.
 The conclusion is entirely in pale green because although it’s changed, no tokens were added
@@ -665,15 +666,24 @@ new, no line of old text is shown for them.
   .. image:: ../_static/diffs-coqtop-on3.png
      :alt: coqtop with Set Diffs on
 
+This image shows an error message with diff highlighting in CoqIDE:
+
+..
+
+  .. image:: ../_static/diffs-error-message.png
+     :alt: |CoqIDE| error message with diffs
+
 How to enable diffs
 ```````````````````
 
 .. opt:: Diffs %( "on" %| "off" %| "removed" %)
    :name: Diffs
 
-   The “on” option highlights added tokens in green, while the “removed” option
+   The “on” setting highlights added tokens in green, while the “removed” setting
    additionally reprints items with removed tokens in red.  Unchanged tokens in
-   modified items are shown with pale green or red.  (Colors are user-configurable.)
+   modified items are shown with pale green or red.  Diffs in error messages
+   use red and green for the compared values; they appear regardless of the setting.
+   (Colors are user-configurable.)
 
 For coqtop, showing diffs can be enabled when starting coqtop with the
 ``-diffs on|off|removed`` command-line option or by setting the :opt:`Diffs` option
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index 878e9f477b..07cdc1e8a3 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -39,6 +39,13 @@ uses strikeout on removed text.
 
 open Pp_diff
 
+let term_color = ref true
+
+let write_color_enabled enabled =
+  term_color := enabled
+
+let color_enabled () = !term_color
+
 let diff_option = ref `OFF
 
 let read_diffs_option () = match !diff_option with
@@ -46,11 +53,18 @@ let read_diffs_option () = match !diff_option with
 | `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 write_diffs_option opt =
+  let enable opt =
+    if not (color_enabled ()) then
+      CErrors.user_err Pp.(str "Enabling Diffs requires setting the \"-color\" command line argument to \"on\" or \"auto\".")
+    else
+      diff_option := opt
+  in
+  match opt with
+  | "off" -> diff_option := `OFF
+  | "on" -> enable `ON
+  | "removed" -> enable `REMOVED
+  | _ -> CErrors.user_err Pp.(str "Diffs option only accepts the following values: \"off\", \"on\", \"removed\".")
 
 let () =
   Goptions.(declare_string_option {
diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli
index 1ebde3d572..fd10eaa458 100644
--- a/printing/proof_diffs.mli
+++ b/printing/proof_diffs.mli
@@ -16,6 +16,12 @@ val write_diffs_option : string -> unit
 (** Returns true if the diffs option is "on" or "removed" *)
 val show_diffs : unit -> bool
 
+(** controls whether color output is enabled *)
+val write_color_enabled : bool -> unit
+
+(** true indicates that color output is enabled *)
+val color_enabled : unit -> bool
+
 open Evd
 open Environ
 open Constr
diff --git a/test-suite/output/Error_msg_diffs.out b/test-suite/output/Error_msg_diffs.out
new file mode 100644
index 0000000000..3e337e892d
--- /dev/null
+++ b/test-suite/output/Error_msg_diffs.out
@@ -0,0 +1,12 @@
+File "stdin", line 32, characters 0-12:
+Error:
+In environment
+T : Type
+p : T -> bool
+a : T
+t1, t2 : btree T
+IH1 : count p (rev_tree t1) = count p t1
+IH2 : count p (rev_tree t2) = count p t2
+Unable to unify "(if p a then 1 else 0) + (count p t1 + count p t2)" with
+ "(if p a then 1 else 0) + (count p t2 + count p t1)".
+
diff --git a/test-suite/output/Error_msg_diffs.v b/test-suite/output/Error_msg_diffs.v
new file mode 100644
index 0000000000..11c766b210
--- /dev/null
+++ b/test-suite/output/Error_msg_diffs.v
@@ -0,0 +1,35 @@
+(* coq-prog-args: ("-color" "on" "-async-proofs" "off") *)
+(* Re: -async-proofs off, see https://github.com/coq/coq/issues/9671 *)
+(* Shows diffs in an error message for an "Unable to unify" error *)
+Require Import Arith List Bool.
+
+Inductive btree (T : Type) : Type :=
+  Leaf | Node (val : T) (t1 t2 : btree T).
+
+Arguments Leaf {T}.
+Arguments Node {T}.
+
+Fixpoint rev_tree {T : Type} (t : btree T) : btree T :=
+match t with
+| Leaf => Leaf
+| Node x t1 t2 => Node x (rev_tree t2) (rev_tree t1)
+end.
+
+Fixpoint count {T : Type} (p : T -> bool) (t : btree T) : nat :=
+match t with
+| Leaf => 0
+| Node x t1 t2 =>
+  (if p x then 1 else 0) + (count p t1 + count p t2)
+end.
+
+Lemma count_rev_tree {T} (p : T -> bool) t : count p (rev_tree t) = count p t.
+Proof.
+induction t as [ | a t1 IH1 t2 IH2].
+  easy.
+simpl.
+rewrite IH1.
+rewrite IH2.
+reflexivity.
+rewrite (Nat.add_comm (count p t2)).
+easy.
+Qed.
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index f2c24807b8..c1737b6d8a 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -95,9 +95,11 @@ let init_color opts =
       | Some s -> Topfmt.parse_color_config s; true   (* Overwrite all colors *)
     end
     else begin
-      Topfmt.default_styles (); false                 (** textual markers, no color *)
+      Topfmt.default_styles (); false                 (* textual markers, no color *)
     end
   in
+  if not term_color then
+    Proof_diffs.write_color_enabled term_color;
   if Proof_diffs.show_diffs () && not term_color then
     (prerr_endline "Error: -diffs requires enabling -color"; exit 1);
   Topfmt.init_terminal_output ~color:term_color
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 9dd321be51..6396240f68 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -125,7 +125,7 @@ let display_eq ~flags env sigma t1 t2 =
 let rec pr_explicit_aux env sigma t1 t2 = function
 | [] ->
   (* no specified flags: default. *)
-  (quote (Printer.pr_leconstr_env env sigma t1), quote (Printer.pr_leconstr_env env sigma t2))
+  Printer.pr_leconstr_env env sigma t1, Printer.pr_leconstr_env env sigma t2
 | flags :: rem ->
   let equal = display_eq ~flags env sigma t1 t2 in
   if equal then
@@ -137,7 +137,7 @@ let rec pr_explicit_aux env sigma t1 t2 = function
     in
     let ct2 = Flags.with_options flags (fun () -> extern_constr false env sigma t2) ()
     in
-    quote (Ppconstr.pr_lconstr_expr ct1), quote (Ppconstr.pr_lconstr_expr ct2)
+    Ppconstr.pr_lconstr_expr ct1, Ppconstr.pr_lconstr_expr ct2
 
 let explicit_flags =
   let open Constrextern in
@@ -148,8 +148,25 @@ let explicit_flags =
     [print_implicits; print_coercions; print_no_symbol]; (* Then more! *)
     [print_universes; print_implicits; print_coercions; print_no_symbol] (* and more! *) ]
 
+let with_diffs pm pn =
+  try
+    let tokenize_string = Proof_diffs.tokenize_string in
+    Pp_diff.diff_pp ~tokenize_string pm pn
+  with Pp_diff.Diff_Failure msg ->
+    begin
+      try ignore(Sys.getenv("HIDEDIFFFAILUREMSG"))
+      with Not_found ->
+        Feedback.msg_warning Pp.(
+            hov 0 (str ("Diff failure: " ^ msg) ++ spc () ++
+            hov 0 (str "Showing message without diff highlighting" ++ spc () ++
+            hov 0 (str "Please report at " ++ str Coq_config.wwwbugtracker ++ str "."))))
+    end;
+    pm, pn
+
 let pr_explicit env sigma t1 t2 =
-  pr_explicit_aux env sigma t1 t2 explicit_flags
+  let p1, p2 = pr_explicit_aux env sigma t1 t2 explicit_flags in
+  let p1, p2 = with_diffs p1 p2 in
+  quote p1, quote p2
 
 let pr_db env i =
   try
@@ -1054,10 +1071,11 @@ let pr_constr_exprs exprs =
          exprs (mt ()))
 
 let explain_mismatched_contexts env c i j =
+  let pm, pn = with_diffs (pr_rel_context env (Evd.from_env env) j) (pr_constr_exprs i) in
   str"Mismatched contexts while declaring instance: " ++ brk (1,1) ++
-    hov 1 (str"Expected:" ++ brk (1, 1) ++ pr_rel_context env (Evd.from_env env) j) ++
+    hov 1 (str"Expected:" ++ brk (1, 1) ++ pm) ++
     fnl () ++ brk (1,1) ++
-    hov 1 (str"Found:" ++ brk (1, 1) ++ pr_constr_exprs i)
+    hov 1 (str"Found:" ++ brk (1, 1) ++ pn)
 
 let explain_typeclass_error env = function
   | NotAClass c -> explain_not_a_class env c
@@ -1066,10 +1084,11 @@ let explain_typeclass_error env = function
 (* Refiner errors *)
 
 let explain_refiner_bad_type env sigma arg ty conclty =
+  let pm, pn = with_diffs (pr_lconstr_env env sigma ty) (pr_lconstr_env env sigma conclty) in
   str "Refiner was given an argument" ++ brk(1,1) ++
   pr_lconstr_env env sigma arg ++ spc () ++
-  str "of type" ++ brk(1,1) ++ pr_lconstr_env env sigma ty ++ spc () ++
-  str "instead of" ++ brk(1,1) ++ pr_lconstr_env env sigma conclty ++ str "."
+  str "of type" ++ brk(1,1) ++ pm ++ spc () ++
+  str "instead of" ++ brk(1,1) ++ pn ++ str "."
 
 let explain_refiner_unresolved_bindings l =
   str "Unable to find an instance for the " ++