10 files changed, 56 insertions, 12 deletions
diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v
index 05eeaac631..bd9240476f 100644
--- a/test-suite/output/Arguments.v
+++ b/test-suite/output/Arguments.v
@@ -17,7 +17,7 @@ Definition fcomp A B C f (g : A -> B) (x : A) : C := f (g x).
 Arguments fcomp {_ _ _}%type_scope f g x /.
 About fcomp.
 Definition volatile := fun x : nat => x.
-Arguments volatile /.
+Arguments volatile / _.
 About volatile.
 Set Implicit Arguments.
 Section S1.
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index 3488cb3056..1633ad9765 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -1,9 +1,20 @@
+File "stdin", line 1, characters 0-36:
+Warning: Ignoring rename of x into y. Only implicit arguments can be renamed.
+[arguments-ignore-rename-nonimpl,vernacular]
 The command has indeed failed with message:
 Error: To rename arguments the "rename" flag must be specified.
 Argument A renamed to B.
-The command has indeed failed with message:
-Error: To rename arguments the "rename" flag must be specified.
-Argument A renamed to T.
+File "stdin", line 2, characters 0-25:
+Warning: Ignoring rename of A into T. Only implicit arguments can be renamed.
+[arguments-ignore-rename-nonimpl,vernacular]
+File "stdin", line 2, characters 0-25:
+Warning: This command is just asserting the number and names of arguments of
+identity. If this is what you want add ': assert' to silence the warning. If
+you want to clear implicit arguments add ': clear implicits'. If you want to
+clear notation scopes add ': clear scopes' [arguments-assert,vernacular]
+File "stdin", line 4, characters 0-40:
+Warning: Ignoring rename of x into y. Only implicit arguments can be renamed.
+[arguments-ignore-rename-nonimpl,vernacular]
 @eq_refl
      : forall (B : Type) (y : B), y = y
 eq_refl
@@ -110,6 +121,9 @@ The command has indeed failed with message:
 Error: Argument z cannot be declared implicit.
 The command has indeed failed with message:
 Error: Extra argument y.
+File "stdin", line 53, characters 0-26:
+Warning: Ignoring rename of x into s. Only implicit arguments can be renamed.
+[arguments-ignore-rename-nonimpl,vernacular]
 The command has indeed failed with message:
 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 b6fbeb6ec7..e42c983361 100644
--- a/test-suite/output/Arguments_renaming.v
+++ b/test-suite/output/Arguments_renaming.v
@@ -1,5 +1,5 @@
 Fail Arguments eq_refl {B y}, [B] y.
-Fail Arguments identity T _ _.
+Arguments identity T _ _.
 Arguments eq_refl A x : assert.
 Arguments eq_refl {B y}, [B] y : rename.
 
diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out
index 62e9ef4b20..06a6b2d157 100644
--- a/test-suite/output/Errors.out
+++ b/test-suite/output/Errors.out
@@ -6,5 +6,5 @@ The command has indeed failed with message:
 In nested Ltac calls to "f" and "apply x", last call failed.
 Unable to unify "nat" with "True".
 The command has indeed failed with message:
-Ltac call to "instantiate" failed.
+Ltac call to "instantiate ( (ident) := (lglob) )" failed.
 Error: Instance is not well-typed in the environment of ?x.
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index 20101f48e5..5541ccf57b 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -58,3 +58,5 @@ exist (Q x) y conj
      : nat -> nat
 % j
      : nat -> nat
+{1, 2}
+     : nat -> Prop
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index 3cf89818d9..1d8278c088 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -111,3 +111,8 @@ Check (exist (Q x) y conj).
 Notation "% i" := (fun i : nat => i) (at level 0, i ident).
 Check %i.
 Check %j.
+
+(* Check bug raised on coq-club on Sep 12, 2016 *)
+
+Notation "{ x , y , .. , v }" := (fun a => (or .. (or (a = x) (a = y)) .. (a = v))).
+Check ({1, 2}).
diff --git a/test-suite/output/PrintModule.out b/test-suite/output/PrintModule.out
index db464fd07e..751d5fcc48 100644
--- a/test-suite/output/PrintModule.out
+++ b/test-suite/output/PrintModule.out
@@ -2,3 +2,4 @@ Module N : S with Definition T := nat := M
 
 Module N : S with Module T := K := M
 
+Module Type Func = Funsig (T0:Test) Sig Parameter x : T0.t. End
diff --git a/test-suite/output/PrintModule.v b/test-suite/output/PrintModule.v
index 999d9a9862..5f30f7cda6 100644
--- a/test-suite/output/PrintModule.v
+++ b/test-suite/output/PrintModule.v
@@ -32,3 +32,19 @@ Module N : S with Module T := K := M.
 Print Module N.
 
 End BAR.
+
+Module QUX.
+
+Module Type Test.
+  Parameter t : Type.
+End Test.
+
+Module Type Func (T:Test).
+  Parameter x : T.t.
+End Func.
+
+Module Shortest_path (T : Test).
+Print Func.
+End Shortest_path.
+
+End QUX.
diff --git a/test-suite/output/inference.v b/test-suite/output/inference.v
index cd9a4a12b2..1825db1676 100644
--- a/test-suite/output/inference.v
+++ b/test-suite/output/inference.v
@@ -14,6 +14,7 @@ Definition P (e:option L) :=
 Print P.
 
 (* Check that plus is folded even if reduction is involved *)
+Set Refolding Reduction.
 Check (fun m n p (H : S m <= (S n) + p) => le_S_n _ _ H).
 
 
diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out
index 21554e9ff8..f4254e4e2f 100644
--- a/test-suite/output/ltac.out
+++ b/test-suite/output/ltac.out
@@ -4,20 +4,25 @@ Ltac f x y z :=
   symmetry in x, y; auto with z; auto; intros **; clearbody x; generalize
    dependent z
 The command has indeed failed with message:
-In nested Ltac calls to "g1" and "refine", last call failed.
+In nested Ltac calls to "g1" and "refine (uconstr)", last call failed.
 The term "I" has type "True" while it is expected to have type "False".
 The command has indeed failed with message:
-In nested Ltac calls to "f1" and "refine", last call failed.
+In nested Ltac calls to "f1 (constr)" and "refine (uconstr)", last call
+failed.
 The term "I" has type "True" while it is expected to have type "False".
 The command has indeed failed with message:
-In nested Ltac calls to "g2", "g1" and "refine", last call failed.
+In nested Ltac calls to "g2 (constr)", "g1" and "refine (uconstr)", last call
+failed.
 The term "I" has type "True" while it is expected to have type "False".
 The command has indeed failed with message:
-In nested Ltac calls to "f2", "f1" and "refine", last call failed.
+In nested Ltac calls to "f2", "f1 (constr)" and "refine (uconstr)", last call
+failed.
 The term "I" has type "True" while it is expected to have type "False".
 The command has indeed failed with message:
-In nested Ltac calls to "h" and "injection", last call failed.
+In nested Ltac calls to "h" and "injection (destruction_arg)", last call
+failed.
 Error: No primitive equality found.
 The command has indeed failed with message:
-In nested Ltac calls to "h" and "injection", last call failed.
+In nested Ltac calls to "h" and "injection (destruction_arg)", last call
+failed.
 Error: No primitive equality found.