14 files changed, 156 insertions, 44 deletions
diff --git a/test-suite/bugs/closed/bug_11553.v b/test-suite/bugs/closed/bug_11553.v
new file mode 100644
index 0000000000..a4a4353cd6
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11553.v
@@ -0,0 +1,34 @@
+Definition var := nat.
+Module Import A.
+Class Rename (term : Type) := rename : (var -> var) -> term -> term.
+End A.
+
+Inductive tm : Type :=
+  (* | tv : vl_ -> tm *)
+ with vl_ : Type :=
+  | var_vl : var -> vl_.
+
+Definition vl := vl_.
+
+Fixpoint tm_rename (sb : var -> var) (t : tm) : tm :=
+  let b := vl_rename : Rename vl in
+  match t with
+  end
+with
+vl_rename (sb : var -> var) v : vl :=
+  let a := tm_rename : Rename tm in
+  let b := vl_rename : Rename vl in
+  match v with
+  | var_vl x => var_vl (sb x)
+  end.
+
+Instance rename_vl : Rename vl := vl_rename.
+
+Lemma foo ξ x: rename_vl ξ (var_vl x) = var_vl x.
+(* Succeeds *)
+cbn. Abort.
+
+Lemma foo ξ x: rename ξ (var_vl x) = var_vl x.
+(* Fails *)
+cbn.
+Abort.
diff --git a/test-suite/failure/Template.v b/test-suite/failure/Template.v
deleted file mode 100644
index fbd9c8bcba..0000000000
--- a/test-suite/failure/Template.v
+++ /dev/null
@@ -1,28 +0,0 @@
-
-Module TestUnsetTemplateCheck.
-  Unset Template Check.
-
-  Section Foo.
-
-    Context (A : Type).
-
-    Definition cstr := nat : ltac:(let ty := type of A in exact ty).
-
-    Inductive myind :=
-    | cons : A -> myind.
-  End Foo.
-
-  (* Can only succeed if no template check is performed *)
-  Check myind True : Prop.
-
-  About myind.
-
-  (* test discharge puts things in the right order (by using the
-     checker on the result) *)
-  Section S.
-
-    Variables (A:Type) (a:A).
-    Inductive bb (B:Type) := BB : forall a', a = a' -> B -> bb B.
-  End S.
-
-End TestUnsetTemplateCheck.
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 *)
 
diff --git a/test-suite/success/Generalization.v b/test-suite/success/Generalization.v
index de34e007d2..df729588f4 100644
--- a/test-suite/success/Generalization.v
+++ b/test-suite/success/Generalization.v
@@ -11,4 +11,10 @@ Admitted.
 Print a_eq_b.
 
 
+Require Import Morphisms.
 
+Class Equiv A := equiv : A -> A -> Prop.
+Class Setoid A `{Equiv A} := setoid_equiv:> Equivalence (equiv).
+
+Lemma vcons_proper A `[Equiv A] `[!Setoid A] (x : True) : True.
+Admitted.
diff --git a/test-suite/success/ImplicitArguments.v b/test-suite/success/ImplicitArguments.v
index b16e4a1186..e68040e4d4 100644
--- a/test-suite/success/ImplicitArguments.v
+++ b/test-suite/success/ImplicitArguments.v
@@ -1,3 +1,15 @@
+
+Axiom foo : forall (x y z t : nat), nat.
+
+Arguments foo {_} _ [z] t.
+Check (foo 1).
+Arguments foo {_} _ {z} {t}.
+Fail Arguments foo {_} _ [z] {t}.
+Check (foo 1).
+
+Definition foo1 [m] n := n + m.
+Check (foo1 1).
+
 Inductive vector {A : Type} : nat -> Type :=
 | vnil : vector 0
 | vcons : A -> forall {n'}, vector n' -> vector (S n').
@@ -33,3 +45,11 @@ Abort.
 
 Inductive A {P:forall m {n}, n=m -> Prop} := C : P 0 eq_refl -> A.
 Inductive B (P:forall m {n}, n=m -> Prop) := D : P 0 eq_refl -> B P.
+
+Inductive A' {P:forall m [n], n=m -> Prop} := C' : P 0 eq_refl -> A'.
+Inductive A'' [P:forall m {n}, n=m -> Prop] (b : bool):= C'' : P 0 eq_refl -> A'' b.
+Inductive A''' (P:forall m [n], n=m -> Prop) (b : bool):= C''' : P 0 eq_refl -> A''' P b.
+
+Definition F (id: forall [A] [x : A], A) := id.
+Definition G := let id := (fun [A] (x : A) => x) in id.
+Fail Definition G' := let id := (fun {A} (x : A) => x) in id.
diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v
index ecaaedca53..59650d6822 100644
--- a/test-suite/success/implicit.v
+++ b/test-suite/success/implicit.v
@@ -114,9 +114,13 @@ Check h 0.
 Inductive I {A} (a:A) : forall {n:nat}, Prop :=
  | C : I a (n:=0).
 
+Inductive I' [A] (a:A) : forall [n:nat], n =0 -> Prop :=
+ | C' : I' a eq_refl.
+
 Inductive I2 (x:=0) : Prop :=
- | C2 {p:nat} : p = 0 -> I2.
-Check C2 eq_refl.
+ | C2 {p:nat} : p = 0 -> I2
+ | C2' [p:nat] : p = 0 -> I2.
+Check C2' eq_refl.
 
 Inductive I3 {A} (x:=0) (a:A) : forall {n:nat}, Prop :=
  | C3 : I3 a (n:=0).
@@ -147,6 +151,7 @@ Set Warnings "syntax".
 (* Miscellaneous tests *)
 
 Check let f := fun {x:nat} y => y=true in f false.
+Check let f := fun [x:nat] y => y=true in f false.
 
 (* Isn't the name "arg_1" a bit fragile, here? *)
 
@@ -157,3 +162,23 @@ Check fun f : forall {_:nat}, nat => f (arg_1:=0).
 Set Warnings "+syntax".
 Check id (fun x => let f c {a} (b:a=a) := b in f true (eq_refl 0)).
 Set Warnings "syntax".
+
+
+Axiom eq0le0 : forall (n : nat) (x : n = 0), n <= 0.
+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.