18 files changed, 878 insertions, 16 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/Notations.out b/test-suite/output/Notations.out
index 94b86fc222..b870fa6f6f 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -137,3 +137,71 @@ end = p
      : forall x : nat, x = x -> Prop
 bar  0
      : nat
+let k := rew [P] p in v in k
+     : P y
+let k := rew [P] p in v in k
+     : P y
+let k := rew <- [P] p in v' in k
+     : P x
+let k := rew [P] p in v in k
+     : P y
+let k := rew [P] p in v in k
+     : P y
+let k := rew <- [P] p in v' in k
+     : P x
+let k := rew [fun y : A => P y] p in v in k
+     : P y
+let k := rew [fun y : A => P y] p in v in k
+     : P y
+let k := rew <- [fun y : A => P y] p in v' in k
+     : P x
+let k := rew [fun y : A => P y] p in v in k
+     : P y
+let k := rew [fun y : A => P y] p in v in k
+     : P y
+let k := rew <- [fun y : A => P y] p in v' in k
+     : P x
+let k := rew dependent [P] p in v in k
+     : P y p
+let k := rew dependent [P] p in v in k
+     : P y p
+let k := rew dependent <- [P'] p in v' in k
+     : P' x (eq_sym p)
+let k := rew dependent [P] p in v in k
+     : P y p
+let k := rew dependent [P] p in v in k
+     : P y p
+let k := rew dependent <- [P'] p in v' in k
+     : P' x (eq_sym p)
+let k := rew dependent [P] p in v in k
+     : P y p
+let k := rew dependent [P] p in v in k
+     : P y p
+let k := rew dependent <- [P'] p in v' in k
+     : P' x (eq_sym p)
+let k := rew dependent [fun y p => id (P y p)] p in v in k
+     : P y p
+let k := rew dependent [fun y p => id (P y p)] p in v in k
+     : P y p
+let k := rew dependent <- [fun y0 p => id (P' y0 p)] p in v' in k
+     : P' x (eq_sym p)
+let k := rew dependent [P] p in v in k
+     : P y p
+let k := rew dependent [P] p in v in k
+     : P y p
+let k := rew dependent <- [P'] p in v' in k
+     : P' x (eq_sym p)
+let k := rew dependent [fun y p0 => id (P y p0)] p in v in k
+     : P y p
+let k := rew dependent [fun y p0 => id (P y p0)] p in v in k
+     : P y p
+let k := rew dependent <- [fun y0 p0 => id (P' y0 p0)] p in v' in k
+     : P' x (eq_sym p)
+rew dependent [P] p in v
+     : P y p
+rew dependent <- [P'] p in v'
+     : P' x (eq_sym p)
+rew dependent [fun a x => id (P a x)] p in v
+     : id (P y p)
+rew dependent <- [fun a p' => id (P' a p')] p in v'
+     : id (P' x (eq_sym p))
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index adab324cf0..7d2f1e9ba8 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -251,11 +251,11 @@ Notation NONE := None.
 Check (fun x => match x with SOME x => x | NONE => 0 end).
 
 Notation NONE2 := (@None _).
-Notation SOME2 := (@Some _).     
+Notation SOME2 := (@Some _).
 Check (fun x => match x with SOME2 x => x | NONE2 => 0 end).
 
 Notation NONE3 := @None.
-Notation SOME3 := @Some.     
+Notation SOME3 := @Some.
 Check (fun x => match x with SOME3 _ x => x | NONE3 _ => 0 end).
 
 Notation "a :'" := (cons a) (at level 12).
@@ -300,3 +300,61 @@ Definition bar (a b : nat) := plus a b.
 Notation "" := A (format "", only printing).
 Check (bar A 0).
 End M.
+
+(* Check eq notations *)
+Module EqNotationsCheck.
+  Import EqNotations.
+  Section nd.
+    Context (A : Type) (x : A) (P : A -> Type)
+            (y : A) (p : x = y) (v : P x) (v' : P y).
+
+    Check let k : P y := rew p in v in k.
+    Check let k : P y := rew -> p in v in k.
+    Check let k : P x := rew <- p in v' in k.
+    Check let k : P y := rew [P] p in v in k.
+    Check let k : P y := rew -> [P] p in v in k.
+    Check let k : P x := rew <- [P] p in v' in k.
+    Check let k : P y := rew [fun y => P y] p in v in k.
+    Check let k : P y := rew -> [fun y => P y] p in v in k.
+    Check let k : P x := rew <- [fun y => P y] p in v' in k.
+    Check let k : P y := rew [fun (y : A) => P y] p in v in k.
+    Check let k : P y := rew -> [fun (y : A) => P y] p in v in k.
+    Check let k : P x := rew <- [fun (y : A) => P y] p in v' in k.
+  End nd.
+  Section dep.
+    Context (A : Type) (x : A) (P : forall y, x = y -> Type)
+            (y : A) (p : x = y) (P' : forall x, y = x -> Type)
+            (v : P x eq_refl) (v' : P' y eq_refl).
+
+    Check let k : P y p := rew dependent p in v in k.
+    Check let k : P y p := rew dependent -> p in v in k.
+    Check let k : P' x (eq_sym p) := rew dependent <- p in v' in k.
+    Check let k : P y p := rew dependent [P] p in v in k.
+    Check let k : P y p := rew dependent -> [P] p in v in k.
+    Check let k : P' x (eq_sym p) := rew dependent <- [P'] p in v' in k.
+    Check let k : P y p := rew dependent [fun y p => P y p] p in v in k.
+    Check let k : P y p := rew dependent -> [fun y p => P y p] p in v in k.
+    Check let k : P' x (eq_sym p) := rew dependent <- [fun y p => P' y p] p in v' in k.
+    Check let k : P y p := rew dependent [fun y p => id (P y p)] p in v in k.
+    Check let k : P y p := rew dependent -> [fun y p => id (P y p)] p in v in k.
+    Check let k : P' x (eq_sym p) := rew dependent <- [fun y p => id (P' y p)] p in v' in k.
+    Check let k : P y p := rew dependent [(fun (y : A) (p : x = y) => P y p)] p in v in k.
+    Check let k : P y p := rew dependent -> [(fun (y : A) (p : x = y) => P y p)] p in v in k.
+    Check let k : P' x (eq_sym p) := rew dependent <- [(fun (x : A) (p : y = x) => P' x p)] p in v' in k.
+    Check let k : P y p := rew dependent [(fun (y : A) (p : x = y) => id (P y p))] p in v in k.
+    Check let k : P y p := rew dependent -> [(fun (y : A) (p : x = y) => id (P y p))] p in v in k.
+    Check let k : P' x (eq_sym p) := rew dependent <- [(fun (x : A) (p : y = x) => id (P' x p))] p in v' in k.
+    Check match p as x in _ = a return P a x with
+          | eq_refl => v
+          end.
+    Check match eq_sym p as p' in _ = a return P' a p' with
+          | eq_refl => v'
+          end.
+    Check match p as x in _ = a return id (P a x) with
+          | eq_refl => v
+          end.
+    Check match eq_sym p as p' in _ = a return id (P' a p') with
+          | eq_refl => v'
+          end.
+  End dep.
+End EqNotationsCheck.
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 799d310fa7..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
@@ -63,3 +63,11 @@ fun '{| |} => true
      : R -> bool
 b = a
      : Prop
+The command has indeed failed with message:
+The format is not the same on the right- and left-hand sides of the special token "..".
+The command has indeed failed with message:
+The format is not the same on the right- and left-hand sides of the special token "..".
+The command has indeed failed with message:
+The format is not the same on the right- and left-hand sides of the special token "..".
+The command has indeed failed with message:
+The format is not the same on the right- and left-hand sides of the special token "..".
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 26c7840a16..4de6ce19b4 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -158,3 +158,29 @@ Check b = a.
 End Test.
 
 End L.
+
+Module M.
+
+(* Accept boxes around the end variables of a recursive notation (if equal boxes) *)
+
+Notation " {@ T1 ; T2 ; .. ; Tn } " :=
+  (and T1 (and T2 .. (and Tn True)..))
+  (format "'[v' {@  '[' T1 ']'  ;  '//' '['  T2  ']'  ;  '//' ..  ;   '//' '['  Tn  ']'  } ']'").
+
+Fail Notation " {@ T1 ; T2 ; .. ; Tn } " :=
+  (and T1 (and T2 .. (and Tn True)..))
+  (format "'[v' {@  '[' T1 ']'  ;  '//' '['  T2  ']'  ;  '//' ..  ;   '//' '['  Tn   ']'  } ']'").
+
+Fail Notation " {@ T1 ; T2 ; .. ; Tn } " :=
+  (and T1 (and T2 .. (and Tn True)..))
+  (format "'[v' {@  '[' T1 ']'  ;  '//' '['  T2  ']'  ;  '//' ..  ;   '//' '[v'  Tn  ']'  } ']'").
+
+Fail Notation " {@ T1 ; T2 ; .. ; Tn } " :=
+  (and T1 (and T2 .. (and Tn True)..))
+  (format "'[v' {@  '[' T1 ']'  ;  '//' '['  T2  ']'  ;  '//' ..  ;   '//' '['   Tn  ']'  } ']'").
+
+Fail Notation " {@ T1 ; T2 ; .. ; Tn } " :=
+  (and T1 (and T2 .. (and Tn True)..))
+  (format "'[v' {@  '[' T1 ']'  ;  '//' '['  T2  ']'   ;  '//' ..  ;   '//' '['  Tn  ']'  } ']'").
+
+End M.
diff --git a/test-suite/output/Notations5.out b/test-suite/output/Notations5.out
new file mode 100644
index 0000000000..83dd2f40fb
--- /dev/null
+++ b/test-suite/output/Notations5.out
@@ -0,0 +1,248 @@
+p 0 0 true
+     : 0 = 0 /\ true = true
+p 0 0
+     : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
+p 0
+     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
+p 0 0 (B:=bool)
+     : forall b : bool, 0 = 0 /\ b = b
+p 0 0 (B:=bool)
+     : forall b : bool, 0 = 0 /\ b = b
+p (A:=nat)
+     : forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b
+p (A:=nat)
+     : forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b
+@p nat 0 0
+     : forall (B : Type) (b : B), 0 = 0 /\ b = b
+@p
+     : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
+p 0 0
+     : forall b : bool, 0 = 0 /\ b = b
+p
+     : forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b
+p 0 0 true
+     : 0 = 0 /\ true = true
+p 0 0
+     : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
+p 0
+     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
+p 0 0
+     : forall b : bool, 0 = 0 /\ b = b
+p 0 0
+     : forall b : bool, 0 = 0 /\ b = b
+p
+     : forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b
+p
+     : forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b
+@p nat 0 0
+     : forall (B : Type) (b : B), 0 = 0 /\ b = b
+@p
+     : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
+f x true
+     : 0 = 0 /\ true = true
+f x (B:=bool)
+     : forall b : bool, 0 = 0 /\ b = b
+f x (B:=bool)
+     : forall b : bool, 0 = 0 /\ b = b
+@f nat
+     : forall a1 a2 : nat,
+       T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b
+f (a1:=0) (a2:=0)
+     : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
+f (a1:=0) (a2:=0)
+     : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
+@f
+     : forall (A : Type) (a1 a2 : A),
+       T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b
+f
+     : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
+x.(f) true
+     : 0 = 0 /\ true = true
+x.(f) (B:=bool)
+     : forall b : bool, 0 = 0 /\ b = b
+x.(f) (B:=bool)
+     : forall b : bool, 0 = 0 /\ b = b
+@f nat
+     : forall a1 a2 : nat,
+       T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b
+f (a1:=0) (a2:=0)
+     : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
+f (a1:=0) (a2:=0)
+     : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
+@f
+     : forall (A : Type) (a1 a2 : A),
+       T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b
+f
+     : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
+p
+     : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
+where
+?A : [ |- Type]
+p
+     : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
+where
+?A : [ |- Type]
+u
+     : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
+u
+     : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
+p 0 0
+     : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
+p 0 0
+     : forall b : bool, 0 = 0 /\ b = b
+@p nat 0 0
+     : forall (B : Type) (b : B), 0 = 0 /\ b = b
+@p nat 0 0
+     : forall (B : Type) (b : B), 0 = 0 /\ b = b
+u
+     : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
+where
+?A : [ |- Type]
+u
+     : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
+u
+     : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
+u
+     : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
+where
+?A : [ |- Type]
+u 0 0
+     : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
+u 0 0
+     : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
+@u nat 0 0
+     : forall (B : Type) (b : B), 0 = 0 /\ b = b
+@u nat 0 0
+     : forall (B : Type) (b : B), 0 = 0 /\ b = b
+u 0 0 true
+     : 0 = 0 /\ true = true
+u 0 0 true
+     : 0 = 0 /\ true = true
+v
+     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
+v 0
+     : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
+v 0
+     : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
+v 0 (B:=bool) true
+     : 0 = 0 /\ true = true
+v
+     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
+@v 0
+     : forall (B : Type) (b : B), 0 = 0 /\ b = b
+@v 0
+     : forall (B : Type) (b : B), 0 = 0 /\ b = b
+v 0 (B:=bool)
+     : forall b : bool, 0 = 0 /\ b = b
+v
+     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
+v 0
+     : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
+v 0
+     : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
+v 0 (B:=bool) true
+     : 0 = 0 /\ true = true
+v
+     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
+@v 0
+     : forall (B : Type) (b : B), 0 = 0 /\ b = b
+@v 0
+     : forall (B : Type) (b : B), 0 = 0 /\ b = b
+v 0 (B:=bool)
+     : forall b : bool, 0 = 0 /\ b = b
+##
+     : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
+where
+?A : [ |- Type]
+##
+     : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
+where
+?A : [ |- Type]
+## 0
+     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
+## 0
+     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
+## 0 0
+     : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
+## 0 0
+     : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
+## 0 0 (B:=bool) true
+     : 0 = 0 /\ true = true
+## 0 0 (B:=bool) true
+     : 0 = 0 /\ true = true
+## 0 0 (B:=bool)
+     : forall b : bool, 0 = 0 /\ b = b
+## 0 0 (B:=bool)
+     : forall b : bool, 0 = 0 /\ b = b
+p
+     : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
+where
+?A : [ |- Type]
+##
+     : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
+##
+     : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
+p 0
+     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
+p 0
+     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
+@p nat 0 0
+     : forall (B : Type) (b : B), 0 = 0 /\ b = b
+p 0 0
+     : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
+p 0 0
+     : forall b : ?B, 0 = 0 /\ b = b
+where
+?B : [ |- Type]
+p 0 0 (B:=bool)
+     : forall b : bool, 0 = 0 /\ b = b
+p 0 0 true
+     : 0 = 0 /\ true = true
+## 0
+     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
+## 0
+     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
+## 0 0 (B:=bool)
+     : forall b : bool, 0 = 0 /\ b = b
+## 0 0 (B:=bool)
+     : forall b : bool, 0 = 0 /\ b = b
+## 0 0 (B:=bool) true
+     : 0 = 0 /\ true = true
+## 0 0 (B:=bool) true
+     : 0 = 0 /\ true = true
+## 0
+     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
+## 0
+     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
+## 0 0 (B:=bool)
+     : forall b : bool, 0 = 0 /\ b = b
+## 0 0 (B:=bool)
+     : forall b : bool, 0 = 0 /\ b = b
+## 0 0 (B:=bool) true
+     : 0 = 0 /\ true = true
+## 0 0 (B:=bool) true
+     : 0 = 0 /\ true = true
diff --git a/test-suite/output/Notations5.v b/test-suite/output/Notations5.v
new file mode 100644
index 0000000000..b3bea929ba
--- /dev/null
+++ b/test-suite/output/Notations5.v
@@ -0,0 +1,340 @@
+Module AppliedTermsPrinting.
+
+(* Test different printing paths for applied terms *)
+
+  Module InferredGivenImplicit.
+  Set Implicit Arguments.
+  Set Maximal Implicit Insertion.
+
+  Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b.
+
+  Check p 0 0 true.
+  (* p 0 0 true *)
+  Check p 0 0.
+  (* p 0 0 *)
+  Check p 0.
+  (* p 0 *)
+  Check @p _ 0 0 bool.
+  (* p 0 0 (B:=bool) *)
+  Check p 0 0 (B:=bool).
+  (* p 0 0 (B:=bool) *)
+  Check @p nat.
+  (* p (A:=nat) *)
+  Check p (A:=nat).
+  (* p (A:=nat) *)
+  Check @p _ 0 0.
+  (* @p nat 0 0 *)
+  Check @p.
+  (* @p *)
+
+  Unset Printing Implicit Defensive.
+  Check @p _ 0 0 bool.
+  (* p 0 0 *)
+  Check @p nat.
+  (* p *)
+  Set Printing Implicit Defensive.
+  End InferredGivenImplicit.
+
+  Module ManuallyGivenImplicit.
+  Axiom p : forall {A} (a1 a2:A) {B} (b:B), a1 = a2 /\ b = b.
+
+  Check p 0 0 true.
+  (* p 0 0 true *)
+  Check p 0 0.
+  (* p 0 0 *)
+  Check p 0.
+  (* p 0 *)
+  Check @p _ 0 0 bool.
+  (* p 0 0 *)
+  Check p 0 0 (B:=bool).
+  (* p 0 0 *)
+  Check @p nat.
+  (* p *)
+  Check p (A:=nat).
+  (* p *)
+  Check @p _ 0 0.
+  (* @p nat 0 0 *)
+  Check @p.
+  (* @p *)
+
+  End ManuallyGivenImplicit.
+
+  Module ProjectionWithImplicits.
+  Set Implicit Arguments.
+  Set Maximal Implicit Insertion.
+
+  Record T {A} (a1 a2:A) := { f : forall B (b:B), a1 = a2 /\ b = b }.
+  Parameter x : T 0 0.
+  Check f x true.
+  (* f x true *)
+  Check @f _ _ _ x bool.
+  (* f x (B:=bool) *)
+  Check f x (B:=bool).
+  (* f x (B:=bool) *)
+  Check @f nat.
+  (* @f nat *)
+  Check @f _ 0 0.
+  (* f (a1:=0) (a2:=0) *)
+  Check f (a1:=0) (a2:=0).
+  (* f (a1:=0) (a2:=0) *)
+  Check @f.
+  (* @f *)
+
+  Unset Printing Implicit Defensive.
+  Check f (a1:=0) (a2:=0).
+  (* f *)
+  Set Printing Implicit Defensive.
+
+  Set Printing Projections.
+
+  Check x.(f) true.
+  (* x.(f) true *)
+  Check x.(@f _ _ _) bool.
+  (* x.(f) (B:=bool) *)
+  Check x.(f) (B:=bool).
+  (* x.(f) (B:=bool) *)
+  Check @f nat.
+  (* @f nat *)
+  Check @f _ 0 0.
+  (* f (a1:=0) (a2:=0) *)
+  Check f (a1:=0) (a2:=0).
+  (* f (a1:=0) (a2:=0) *)
+  Check @f.
+  (* @f *)
+
+  Unset Printing Implicit Defensive.
+  Check f (a1:=0) (a2:=0).
+  (* f *)
+
+  End ProjectionWithImplicits.
+
+  Module AtAbbreviationForApplicationHead.
+
+  Axiom p : forall {A} (a1 a2:A) {B} (b:B), a1 = a2 /\ b = b.
+
+  Notation u := @p.
+
+  Check u _.
+  (* p *)
+  Check p.
+  (* p *)
+  Check @p.
+  (* u *)
+  Check u.
+  (* u *)
+  Check p 0 0.
+  (* p 0 0 *)
+  Check u nat 0 0 bool.
+  (* p 0 0 -- WEAKNESS should ideally be (B:=bool) *)
+  Check u nat 0 0.
+  (* @p nat 0 0 *)
+  Check @p nat 0 0.
+  (* @p nat 0 0 *)
+
+  End AtAbbreviationForApplicationHead.
+
+  Module AbbreviationForApplicationHead.
+
+  Set Implicit Arguments.
+  Set Maximal Implicit Insertion.
+
+  Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b.
+
+  Notation u := p.
+
+  Check p.
+  (* u *)
+  Check @p.
+  (* u -- BUG *)
+  Check @u.
+  (* u -- BUG *)
+  Check u.
+  (* u *)
+  Check p 0 0.
+  (* u 0 0 *)
+  Check u 0 0.
+  (* u 0 0 *)
+  Check @p nat 0 0.
+  (* @u nat 0 0 *)
+  Check @u nat 0 0.
+  (* @u nat 0 0 *)
+  Check p 0 0 true.
+  (* u 0 0 true *)
+  Check u 0 0 true.
+  (* u 0 0 true *)
+
+  End AbbreviationForApplicationHead.
+
+  Module AtAbbreviationForPartialApplication.
+
+  Set Implicit Arguments.
+  Set Maximal Implicit Insertion.
+
+  Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b.
+
+  Notation v := (@p _ 0).
+
+  Check v.
+  (* v *)
+  Check p 0 0.
+  (* v 0 *)
+  Check v 0.
+  (* v 0 *)
+  Check v 0 true.
+  (* v 0 (B:=bool) true -- BUG *)
+  Check @p nat 0.
+  (* v *)
+  Check @p nat 0 0.
+  (* @v 0 *)
+  Check @v 0.
+  (* @v 0 *)
+  Check @p nat 0 0 bool.
+  (* v 0 (B:=bool) *)
+
+  End AtAbbreviationForPartialApplication.
+
+  Module AbbreviationForPartialApplication.
+
+  Set Implicit Arguments.
+  Set Maximal Implicit Insertion.
+
+  Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b.
+
+  Notation v := (p 0).
+
+  Check v.
+  (* v *)
+  Check p 0 0.
+  (* v 0 *)
+  Check v 0.
+  (* v 0 *)
+  Check v 0 true.
+  (* v 0 (B:=bool) true -- BUG *)
+  Check @p nat 0.
+  (* v *)
+  Check @p nat 0 0.
+  (* @v 0 *)
+  Check @v 0.
+  (* @v 0 *)
+  Check @p nat 0 0 bool.
+  (* v 0 (B:=bool) *)
+
+  End AbbreviationForPartialApplication.
+
+  Module NotationForHeadApplication.
+
+  Set Implicit Arguments.
+  Set Maximal Implicit Insertion.
+
+  Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b.
+
+  Notation "##" := p (at level 0).
+
+  Check p.
+  (* ## *)
+  Check ##.
+  (* ## *)
+  Check p 0.
+  (* ## 0 *)
+  Check ## 0.
+  (* ## 0 *)
+  Check p 0 0.
+  (* ## 0 0 *)
+  Check ## 0 0.
+  (* ## 0 0 *)
+  Check p 0 0 true.
+  (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *)
+  Check ## 0 0 true.
+  (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *)
+  Check p 0 0 (B:=bool).
+  (* ## 0 0 (B:=bool) *)
+  Check ## 0 0 (B:=bool).
+  (* ## 0 0 (B:=bool) *)
+
+  End NotationForHeadApplication.
+
+  Module AtNotationForHeadApplication.
+
+  Set Implicit Arguments.
+  Set Maximal Implicit Insertion.
+
+  Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b.
+
+  Notation "##" := @p (at level 0).
+
+  Check p.
+  (* p *)
+  Check @p.
+  (* ## *)
+  Check ##.
+  (* ## *)
+  Check p 0.
+  (* p 0 -- why not "## nat 0" *)
+  Check ## nat 0.
+  (* p 0 *)
+  Check ## nat 0 0.
+  (* @p nat 0 0 *)
+  Check p 0 0.
+  (* p 0 0 *)
+  Check ## nat 0 0 _.
+  (* p 0 0 *)
+  Check ## nat 0 0 bool.
+  (* p 0 0 (B:=bool) *)
+  Check ## nat 0 0 bool true.
+  (* p 0 0 true *)
+
+  End AtNotationForHeadApplication.
+
+  Module NotationForPartialApplication.
+
+  Set Implicit Arguments.
+  Set Maximal Implicit Insertion.
+
+  Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b.
+
+  Notation "## q" := (p q) (at level 0, q at level 0).
+
+  Check p 0.
+  (* ## 0 *)
+  Check ## 0.
+  (* ## 0 *)
+  (* Check ## 0 0. *)
+  (* Anomaly *)
+  Check p 0 0 (B:=bool).
+  (* ## 0 0 (B:=bool) *)
+  Check ## 0 0 bool.
+  (* ## 0 0 (B:=bool) -- INCONSISTENT parsing/printing *)
+  Check p 0 0 true.
+  (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *)
+  Check ## 0 0 bool true.
+  (* ## 0 0 (B:=bool) true -- INCONSISTENT parsing/printing + BUG B should not be displayed *)
+
+  End NotationForPartialApplication.
+
+  Module AtNotationForPartialApplication.
+
+  Set Implicit Arguments.
+  Set Maximal Implicit Insertion.
+
+  Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b.
+
+  Notation "## q" := (@p _ q) (at level 0, q at level 0).
+
+  Check p 0.
+  (* ## 0 *)
+  Check ## 0.
+  (* ## 0 *)
+  (* Check ## 0 0. *)
+  (* Anomaly *)
+  Check p 0 0 (B:=bool).
+  (* ## 0 0 (B:=bool) *)
+  Check ## 0 0 bool.
+  (* ## 0 0 (B:=bool) -- INCONSISTENT parsing/printing *)
+  Check p 0 0 true.
+  (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *)
+  Check ## 0 0 bool true.
+  (* ## 0 0 (B:=bool) true -- INCONSISTENCY parsing/printing + BUG B should not be displayed *)
+
+  End AtNotationForPartialApplication.
+
+End AppliedTermsPrinting.
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/output/QArithSyntax.out b/test-suite/output/QArithSyntax.out
new file mode 100644
index 0000000000..6bc04f1cef
--- /dev/null
+++ b/test-suite/output/QArithSyntax.out
@@ -0,0 +1,14 @@
+eq_refl : 102e-2 = 102e-2
+     : 102e-2 = 102e-2
+eq_refl : 102e-1 = 102e-1
+     : 102e-1 = 102e-1
+eq_refl : 1020 = 1020
+     : 1020 = 1020
+eq_refl : 102 = 102
+     : 102 = 102
+eq_refl : 102e-2 = 102e-2
+     : 102e-2 = 102e-2
+eq_refl : -1e-4 = -1e-4
+     : -1e-4 = -1e-4
+eq_refl : -50e-2 = -50e-2
+     : -50e-2 = -50e-2
diff --git a/test-suite/output/QArithSyntax.v b/test-suite/output/QArithSyntax.v
new file mode 100644
index 0000000000..2f2ee0134a
--- /dev/null
+++ b/test-suite/output/QArithSyntax.v
@@ -0,0 +1,9 @@
+Require Import QArith.
+Open Scope Q_scope.
+Check (eq_refl : 1.02 = 102 # 100).
+Check (eq_refl : 1.02e1 = 102 # 10).
+Check (eq_refl : 1.02e+03 = 1020).
+Check (eq_refl : 1.02e+02 = 102 # 1).
+Check (eq_refl : 10.2e-1 = 1.02).
+Check (eq_refl : -0.0001 = -1 # 10000).
+Check (eq_refl : -0.50 = - 50 # 100).
diff --git a/test-suite/output/RealSyntax.out b/test-suite/output/RealSyntax.out
index e6f7556d96..2d877bd813 100644
--- a/test-suite/output/RealSyntax.out
+++ b/test-suite/output/RealSyntax.out
@@ -2,3 +2,17 @@
      : R
 (-31)%R
      : R
+eq_refl : 102e-2 = 102e-2
+     : 102e-2 = 102e-2
+eq_refl : 102e-1 = 102e-1
+     : 102e-1 = 102e-1
+eq_refl : 102e1 = 102e1
+     : 102e1 = 102e1
+eq_refl : 102 = 102
+     : 102 = 102
+eq_refl : 102e-2 = 102e-2
+     : 102e-2 = 102e-2
+eq_refl : -1e-4 = -1e-4
+     : -1e-4 = -1e-4
+eq_refl : -50e-2 = -50e-2
+     : -50e-2 = -50e-2
diff --git a/test-suite/output/RealSyntax.v b/test-suite/output/RealSyntax.v
index 44e8c7a50c..cb3bce70d4 100644
--- a/test-suite/output/RealSyntax.v
+++ b/test-suite/output/RealSyntax.v
@@ -1,3 +1,25 @@
 Require Import Reals.Rdefinitions.
 Check 32%R.
 Check (-31)%R.
+
+Open Scope R_scope.
+
+Check (eq_refl : 1.02 = IZR 102 / IZR (Z.pow_pos 10 2)).
+Check (eq_refl : 1.02e1 = IZR 102 / IZR (Z.pow_pos 10 1)).
+Check (eq_refl : 1.02e+03 = IZR 102 * IZR (Z.pow_pos 10 1)).
+Check (eq_refl : 1.02e+02 = IZR 102).
+Check (eq_refl : 10.2e-1 = 1.02).
+Check (eq_refl : -0.0001 = IZR (-1) / IZR (Z.pow_pos 10 4)).
+Check (eq_refl : -0.50 = IZR (-50) / IZR (Z.pow_pos 10 2)).
+
+Require Import Reals.
+
+Goal 254e3 = 2540 * 10 ^ 2.
+ring.
+Qed.
+
+Require Import Psatz.
+
+Goal 254e3 = 2540 * 10 ^ 2.
+lra.
+Qed.