7 files changed, 50 insertions, 9 deletions
diff --git a/test-suite/README.md b/test-suite/README.md
index a2d5905710..96926f70b9 100644
--- a/test-suite/README.md
+++ b/test-suite/README.md
@@ -67,7 +67,7 @@ See [`test-suite/Makefile`](Makefile) for more information.
 ## Adding a test
 
 Regression tests for closed bugs should be added to
-[`bugs/closed`](bugs/closed), as `1234.v` where `1234` is the bug number.
+[`bugs/closed`](bugs/closed), as `bug_1234.v` where `1234` is the bug number.
 Files in this directory are tested for successful compilation.
 When you fix a bug, you should usually add a regression test here as well.
 
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index 5093e785de..26ebd8efc3 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -86,8 +86,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 number 2 (anonymous in original definition) cannot be declared
-implicit.
+Argument number 3 is a trailing implicit, so it can't be declared non
+maximal. Please use { } instead of [ ].
 The command has indeed failed with message:
 Extra arguments: y.
 The command has indeed failed with message:
diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v
index 9713a9dbbe..6ac09cf771 100644
--- a/test-suite/output/Arguments_renaming.v
+++ b/test-suite/output/Arguments_renaming.v
@@ -49,7 +49,6 @@ 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 : rename.
-Fail Arguments eq {F} x [z] : rename.
+Fail Arguments eq {A} x [z] : rename.
 Fail Arguments eq {F} x z y.
 Fail Arguments eq {R} s t.
-
diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out
index 3f4d5ef58c..190c34262f 100644
--- a/test-suite/output/PrintAssumptions.out
+++ b/test-suite/output/PrintAssumptions.out
@@ -3,6 +3,10 @@ foo : nat
 Axioms:
 foo : nat
 Axioms:
+bli : Type
+Axioms:
+bli : Type
+Axioms:
 extensionality : forall (P Q : Type) (f g : P -> Q),
                  (forall x : P, f x = g x) -> f = g
 Axioms:
diff --git a/test-suite/output/PrintAssumptions.v b/test-suite/output/PrintAssumptions.v
index 3d4dfe603d..4c980fddba 100644
--- a/test-suite/output/PrintAssumptions.v
+++ b/test-suite/output/PrintAssumptions.v
@@ -30,6 +30,21 @@ Module P := N M.
 Print Assumptions M.bar. (* Should answer: foo *)
 Print Assumptions P.bar. (* Should answer: foo *)
 
+(* Print Assumptions used empty instances on polymorphic inductives *)
+Module Poly.
+
+  Set Universe Polymorphism.
+  Axiom bli : Type.
+
+  Definition bla := bli -> bli.
+
+  Inductive blo : bli -> Type := .
+
+  Print Assumptions bla.
+  Print Assumptions blo.
+
+End Poly.
+
 
 (* The original test-case of the bug-report *)
 
diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v
index 668d765d83..59650d6822 100644
--- a/test-suite/success/implicit.v
+++ b/test-suite/success/implicit.v
@@ -169,3 +169,16 @@ Variable eq0le0' : forall (n : nat) {x : n = 0}, n <= 0.
 Axiom eq0le0'' : forall (n : nat) {x : n = 0}, n <= 0.
 Definition eq0le0''' : forall (n : nat) {x : n = 0}, n <= 0. Admitted.
 Fail Axiom eq0le0'''' : forall [n : nat] {x : n = 0}, n <= 0.
+
+Module TestUnnamedImplicit.
+
+Axiom foo : forall A, A -> A.
+
+Arguments foo {A} {_}.
+Check foo (arg_2:=true) : bool.
+Check foo : bool.
+
+Arguments foo {A} {x}.
+Check foo (x:=true) : bool.
+
+End TestUnnamedImplicit.
diff --git a/test-suite/success/uniform_inductive_parameters.v b/test-suite/success/uniform_inductive_parameters.v
index 42236a5313..651247937d 100644
--- a/test-suite/success/uniform_inductive_parameters.v
+++ b/test-suite/success/uniform_inductive_parameters.v
@@ -1,13 +1,23 @@
+Module Att.
+  #[uniform] Inductive list (A : Type) :=
+  | nil : list
+  | cons : A -> list -> list.
+  Check (list : Type -> Type).
+  Check (cons : forall A, A -> list A -> list A).
+End Att.
+
 Set Uniform Inductive Parameters.
 
 Inductive list (A : Type) :=
-  | nil : list
-  | cons : A -> list -> list.
+| nil : list
+| cons : A -> list -> list.
 Check (list : Type -> Type).
 Check (cons : forall A, A -> list A -> list A).
 
 Inductive list2 (A : Type) (A' := prod A A) :=
-  | nil2 : list2
-  | cons2 : A' -> list2 -> list2.
+| nil2 : list2
+| cons2 : A' -> list2 -> list2.
 Check (list2 : Type -> Type).
 Check (cons2 : forall A (A' := prod A A), A' -> list2 A -> list2 A).
+
+#[nonuniform] Inductive bla (n:nat) := c (_ : bla (S n)).