9 files changed, 69 insertions, 14 deletions
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/Fixpoint.out b/test-suite/output/Fixpoint.out
index 6879cbc3c2..60bc9cbf55 100644
--- a/test-suite/output/Fixpoint.out
+++ b/test-suite/output/Fixpoint.out
@@ -1,8 +1,8 @@
-fix F (A B : Set) (f : A -> B) (l : list A) {struct l} : 
-list B := match l with
-          | nil => nil
-          | a :: l0 => f a :: F A B f l0
-          end
+fix F (A B : Set) (f : A -> B) (l : list A) {struct l} : list B :=
+  match l with
+  | nil => nil
+  | a :: l0 => f a :: F A B f l0
+  end
      : forall A B : Set, (A -> B) -> list A -> list B
 let fix f (m : nat) : nat := match m with
                              | 0 => 0
diff --git a/test-suite/output/Naming.out b/test-suite/output/Naming.out
index c142d28ebe..0a989646cf 100644
--- a/test-suite/output/Naming.out
+++ b/test-suite/output/Naming.out
@@ -61,3 +61,18 @@
   H : a = 0 -> forall a : nat, a = 0
   ============================
   a = 0
+File "stdin", line 101, characters 47-48:
+Warning: Ignoring implicit binder declaration in unexpected position.
+[unexpected-implicit-declaration,syntax]
+File "stdin", line 105, characters 36-37:
+Warning: Ignoring implicit binder declaration in unexpected position.
+[unexpected-implicit-declaration,syntax]
+File "stdin", line 106, characters 34-35:
+Warning: Ignoring implicit binder declaration in unexpected position.
+[unexpected-implicit-declaration,syntax]
+File "stdin", line 112, characters 22-23:
+Warning: Ignoring implicit binder declaration in unexpected position.
+[unexpected-implicit-declaration,syntax]
+File "stdin", line 112, characters 30-31:
+Warning: Ignoring implicit binder declaration in unexpected position.
+[unexpected-implicit-declaration,syntax]
diff --git a/test-suite/output/Naming.v b/test-suite/output/Naming.v
index 7f3b332d7d..610fa48c0c 100644
--- a/test-suite/output/Naming.v
+++ b/test-suite/output/Naming.v
@@ -90,3 +90,25 @@ apply H with (a:=a). (* test compliance with printing *)
 Abort.
 
 End A.
+
+Module B.
+
+(* Check valid/invalid implicit arguments *)
+Definition f1 {x} (y:forall {x}, x=0) := x+0.
+Definition f2 := (((fun x => 0):forall {x:nat}, nat), 0).
+Definition f3 := fun {x} (y:forall {x}, x=0) => x+0.
+
+Definition g1 {x} := match x with true => fun {x:bool} => x | false => fun x:bool => x end.
+(* TODO: do not ignore the implicit here *)
+Definition g2 '(x,y) {z} := x+y+z.
+
+Definition h1 := fun x:nat => (fun {x} => x) 0.
+Definition h2 := let g := forall {y}, y=0 in g.
+
+Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..)
+  (at level 200, x binder, y binder, right associativity,
+  format "'[  ' '[  ' ∀  x  ..  y ']' ,  '/' P ']'") : type_scope.
+
+Definition l1 := ∀ {x:nat} {y:nat}, x=0.
+
+End B.
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index aeebc0f98b..839df99ea7 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -219,8 +219,8 @@ Check exists_true '(x,y) (u:=0) '(z,t), x+y=0/\z+t=0.
 Module G.
 Generalizable Variables A R.
 Class Reflexive {A:Type} (R : A->A->Prop) := reflexivity : forall x : A, R x x.
-Check exists_true `{Reflexive A R}, forall x, R x x.
-Check exists_true x `{Reflexive A R} y, x+y=0 -> forall z, R z z.
+Check exists_true `(Reflexive A R), forall x, R x x.
+Check exists_true x `(Reflexive A R) y, x+y=0 -> forall z, R z z.
 End G.
 
 (* Allows recursive patterns for binders to be associative on the left *)
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index 43f88f42a5..f65696e464 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -4,11 +4,11 @@ Entry constr:myconstr is
 [ "6" RIGHTA
   [  ]
 | "5" RIGHTA
-  [ SELF;  "+"; NEXT ]
+  [ SELF; "+"; NEXT ]
 | "4" RIGHTA
-  [ SELF;  "*"; NEXT ]
+  [ SELF; "*"; NEXT ]
 | "3" RIGHTA
-  [  "<"; constr:operconstr LEVEL "10";  ">" ] ]
+  [ "<"; constr:operconstr LEVEL "10"; ">" ] ]
 
 [< b > + < b > * < 2 >]
      : nat
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 *)