Merge branch 'v8.6'

4 files changed, 7 insertions, 8 deletions

diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index 9d90de47c..b084ad498 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -1,6 +1,5 @@
 The command has indeed failed with message:
-Error: To rename arguments the "rename" flag must be
-specified.
+Error: To rename arguments the "rename" flag must be specified.
 Argument A renamed to B.
 File "stdin", line 2, characters 0-25:
 Warning: This command is just asserting the names of arguments of identity.
@@ -104,16 +103,15 @@ Expands to: Constant Top.myplus
 @myplus
      : forall Z : Type, Z -> nat -> nat -> nat
 The command has indeed failed with message:
-Error: Arguments lists should agree on names they provide.
+Error: Argument lists should agree on the names they provide.
 The command has indeed failed with message:
 Error: Sequences of implicit arguments must be of different lengths.
 The command has indeed failed with message:
-Error: Arguments names must be distinct.
+Error: Some argument names are duplicated: F
 The command has indeed failed with message:
 Error: Argument z cannot be declared implicit.
 The command has indeed failed with message:
 Error: Extra arguments: y.
 The command has indeed failed with message:
-Error: To rename arguments the "rename" flag must be
-specified.
+Error: To rename arguments the "rename" flag must be specified.
 Argument A renamed to R.
diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v
index 2d14c94ac..0cb331347 100644
--- a/test-suite/output/Arguments_renaming.v
+++ b/test-suite/output/Arguments_renaming.v
@@ -47,7 +47,7 @@ Check @myplus.
 
 Fail Arguments eq_refl {F g}, [H] k.
 Fail Arguments eq_refl {F}, [F] : rename.
-Fail Arguments eq_refl {F F}, [F] F.
+Fail Arguments eq_refl {F F}, [F] F : rename.
 Fail Arguments eq {F} x [z] : rename.
 Fail Arguments eq {F} x z y.
 Fail Arguments eq {R} s t.
diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v
index fff86d6fa..6fa357a90 100644
--- a/test-suite/output/PatternsInBinders.v
+++ b/test-suite/output/PatternsInBinders.v
@@ -58,7 +58,7 @@ Definition F '(n,p) : Type := (Fin n * Fin p)%type.
 Definition both_z '(n,p) : F (n,p) := (Z _,Z _).
 Print both_z.
 
-(** These tests show examples which do not factorize binders *)
+(** Test factorization of binders *)
 
 Check fun '((x,y) : A*B) '(z,t) => swap (x,y) = (z,t).
 Check forall '(x,y) '((z,t) : B*A), swap (x,y) = (z,t).
diff --git a/test-suite/output/unifconstraints.v b/test-suite/output/unifconstraints.v
index c76fc74a0..b9413a4ac 100644
--- a/test-suite/output/unifconstraints.v
+++ b/test-suite/output/unifconstraints.v
@@ -1,4 +1,5 @@
 (* Set Printing Existential Instances. *)
+Unset Solve Unification Constraints.
 Axiom veeryyyyyyyyyyyyloooooooooooooonggidentifier : nat.
 Goal True /\ True /\ True \/
              veeryyyyyyyyyyyyloooooooooooooonggidentifier =