6 files changed, 82 insertions, 21 deletions

diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index ba4bc070c6..3f0717666c 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -113,7 +113,8 @@ Sequences of implicit arguments must be of different lengths.
 The command has indeed failed with message:
 Some argument names are duplicated: F
 The command has indeed failed with message:
-Argument z cannot be declared implicit.
+Argument number 2 (anonymous in original definition) cannot be declared
+implicit.
 The command has indeed failed with message:
 Extra arguments: y.
 The command has indeed failed with message:
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/test-suite/output/PrintInfos.v b/test-suite/output/PrintInfos.v
index d7c271c3ec..d95cc0e32f 100644
--- a/test-suite/output/PrintInfos.v
+++ b/test-suite/output/PrintInfos.v
@@ -22,7 +22,7 @@ Print comparison.
 Definition foo := forall x, x = 0.
 Parameter bar : foo.
 
-Arguments bar [x].
+Arguments bar {x}.
 About bar.
 Print bar.
 
diff --git a/test-suite/output/RealSyntax.v b/test-suite/output/RealSyntax.v
index 15ae66010e..44e8c7a50c 100644
--- a/test-suite/output/RealSyntax.v
+++ b/test-suite/output/RealSyntax.v
@@ -1,3 +1,3 @@
-Require Import Reals.
+Require Import Reals.Rdefinitions.
 Check 32%R.
 Check (-31)%R.
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index f4544a0df3..ffba1d35cc 100644
--- a/test-suite/output/Search.out
+++ b/test-suite/output/Search.out
@@ -1,59 +1,72 @@
 le_n: forall n : nat, n <= n
 le_0_n: forall n : nat, 0 <= n
 le_S: forall n m : nat, n <= m -> n <= S m
-le_n_S: forall n m : nat, n <= m -> S n <= S m
-le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m
 le_S_n: forall n m : nat, S n <= S m -> n <= m
-min_l: forall n m : nat, n <= m -> Nat.min n m = n
+le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m
+le_n_S: forall n m : nat, n <= m -> S n <= S m
+max_l: forall n m : nat, m <= n -> Nat.max n m = n
 max_r: forall n m : nat, n <= m -> Nat.max n m = m
 min_r: forall n m : nat, m <= n -> Nat.min n m = m
-max_l: forall n m : nat, m <= n -> Nat.max n m = n
+min_l: forall n m : nat, n <= m -> Nat.min n m = n
 le_ind:
   forall (n : nat) (P : nat -> Prop),
   P n ->
   (forall m : nat, n <= m -> P m -> P (S m)) ->
   forall n0 : nat, n <= n0 -> P n0
+le_sind:
+  forall (n : nat) (P : nat -> SProp),
+  P n ->
+  (forall m : nat, n <= m -> P m -> P (S m)) ->
+  forall n0 : nat, n <= n0 -> P n0
 false: bool
 true: bool
+eq_true: bool -> Prop
 is_true: bool -> Prop
 negb: bool -> bool
-eq_true: bool -> Prop
-implb: bool -> bool -> bool
-orb: bool -> bool -> bool
 andb: bool -> bool -> bool
+orb: bool -> bool -> bool
+implb: bool -> bool -> bool
 xorb: bool -> bool -> bool
 Nat.even: nat -> bool
 Nat.odd: nat -> bool
 BoolSpec: Prop -> Prop -> bool -> Prop
-Nat.eqb: nat -> nat -> bool
-Nat.testbit: nat -> nat -> bool
 Nat.ltb: nat -> nat -> bool
+Nat.testbit: nat -> nat -> bool
+Nat.eqb: nat -> nat -> bool
 Nat.leb: nat -> nat -> bool
 Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
-bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b
 bool_rec: forall P : bool -> Set, P true -> P false -> forall b : bool, P b
+eq_true_ind_r:
+  forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true
 eq_true_rec:
   forall P : bool -> Set, P true -> forall b : bool, eq_true b -> P b
-bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b
-eq_true_rect_r:
-  forall (P : bool -> Type) (b : bool), P b -> eq_true b -> P true
-eq_true_rec_r:
-  forall (P : bool -> Set) (b : bool), P b -> eq_true b -> P true
+bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b
 eq_true_rect:
   forall P : bool -> Type, P true -> forall b : bool, eq_true b -> P b
+eq_true_sind:
+  forall P : bool -> SProp, P true -> forall b : bool, eq_true b -> P b
+bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b
 eq_true_ind:
   forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b
-eq_true_ind_r:
-  forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true
+eq_true_rec_r:
+  forall (P : bool -> Set) (b : bool), P b -> eq_true b -> P true
+eq_true_rect_r:
+  forall (P : bool -> Type) (b : bool), P b -> eq_true b -> P true
+bool_sind:
+  forall P : bool -> SProp, P true -> P false -> forall b : bool, P b
 Byte.to_bits:
   Byte.byte ->
   bool * (bool * (bool * (bool * (bool * (bool * (bool * bool))))))
 Byte.of_bits:
   bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))) ->
   Byte.byte
+andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
 andb_true_intro:
   forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true
-andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
+BoolSpec_sind:
+  forall (P Q : Prop) (P0 : bool -> SProp),
+  (P -> P0 true) ->
+  (Q -> P0 false) -> forall b : bool, BoolSpec P Q b -> P0 b
 BoolSpec_ind:
   forall (P Q : Prop) (P0 : bool -> Prop),
   (P -> P0 true) ->