Imported Upstream version 8.6upstream/8.6

44 files changed, 946 insertions, 130 deletions

diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out
index 2c7b04c6..a2ee2d4c 100644
--- a/test-suite/output/Arguments.out
+++ b/test-suite/output/Arguments.out
@@ -101,4 +101,4 @@ Error: Unknown interpretation for notation "$".
 w 3 true = tt
      : Prop
 The command has indeed failed with message:
-Error: Extra argument _.
+Error: Extra arguments: _, _.
diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v
index 05eeaac6..bd924047 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/ArgumentsScope.v b/test-suite/output/ArgumentsScope.v
index 1ff53294..3a90cb79 100644
--- a/test-suite/output/ArgumentsScope.v
+++ b/test-suite/output/ArgumentsScope.v
@@ -11,11 +11,11 @@ About b.
 About negb''.
 About negb'.
 About negb.
-Global Arguments Scope negb'' [ _ ].
-Global Arguments Scope negb' [ _ ].
-Global Arguments Scope negb [ _ ].
-Global Arguments Scope a [ _ ].
-Global Arguments Scope b [ _ ].
+Global Arguments negb'' _ : clear scopes.
+Global Arguments negb' _ : clear scopes.
+Global Arguments negb _ : clear scopes.
+Global Arguments a _ : clear scopes.
+Global Arguments b _ : clear scopes.
 About a.
 About b.
 About negb.
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index 1e3cc37d..b084ad49 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -1,13 +1,17 @@
 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: This command is just asserting the 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]
 @eq_refl
      : forall (B : Type) (y : B), y = y
-@eq_refl nat
-     : forall x : nat, x = x
+eq_refl
+     : ?y = ?y
+where
+?y : [ |- nat] 
 Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
 
 For eq_refl: Arguments are renamed to B, y
@@ -99,15 +103,15 @@ Expands to: Constant Top.myplus
 @myplus
      : forall Z : Type, Z -> nat -> nat -> nat
 The command has indeed failed with message:
-Error: All arguments lists must declare the same names.
+Error: Argument lists should agree on the names they provide.
 The command has indeed failed with message:
-Error: The following arguments are not declared: x.
+Error: Sequences of implicit arguments must be of different lengths.
 The command has indeed failed with message:
-Error: Arguments names must be distinct.
+Error: Some argument names are duplicated: F
 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.
+Error: Extra arguments: y.
 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 e68fbd69..0cb33134 100644
--- a/test-suite/output/Arguments_renaming.v
+++ b/test-suite/output/Arguments_renaming.v
@@ -1,6 +1,6 @@
 Fail Arguments eq_refl {B y}, [B] y.
-Fail Arguments identity T _ _.
-Arguments eq_refl A x.
+Arguments identity A _ _.
+Arguments eq_refl A x : assert.
 Arguments eq_refl {B y}, [B] y : rename.
 
 Check @eq_refl.
@@ -46,9 +46,9 @@ About myplus.
 Check @myplus.
 
 Fail Arguments eq_refl {F g}, [H] k.
-Fail Arguments eq_refl {F}, [F].
-Fail Arguments eq_refl {F F}, [F] F.
-Fail Arguments eq {F} x [z].
+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 {F} x z y.
 Fail Arguments eq {R} s t.
 
diff --git a/test-suite/output/Binder.out b/test-suite/output/Binder.out
new file mode 100644
index 00000000..34558e9a
--- /dev/null
+++ b/test-suite/output/Binder.out
@@ -0,0 +1,8 @@
+foo = fun '(x, y) => x + y
+     : nat * nat -> nat
+forall '(a, b), a /\ b
+     : Prop
+foo = λ '(x, y), x + y
+     : nat * nat → nat
+∀ '(a, b), a ∧ b
+     : Prop
diff --git a/test-suite/output/Binder.v b/test-suite/output/Binder.v
new file mode 100644
index 00000000..9aced9f6
--- /dev/null
+++ b/test-suite/output/Binder.v
@@ -0,0 +1,7 @@
+Definition foo '(x,y) := x + y.
+Print foo.
+Check forall '(a,b), a /\ b.
+
+Require Import Utf8.
+Print foo.
+Check forall '(a,b), a /\ b.
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 09f032d4..8ce6f979 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -6,6 +6,8 @@ fix F (t : t) : P t :=
   end
      : forall P : t -> Type,
        (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t
+
+Argument scopes are [function_scope function_scope _]
      = fun d : TT => match d with
                      | @CTT _ _ b => b
                      end
@@ -24,7 +26,7 @@ match Nat.eq_dec x y with
 end
      : forall (x y : nat) (P : nat -> Type), P x -> P y -> P y
 
-Argument scopes are [nat_scope nat_scope _ _ _]
+Argument scopes are [nat_scope nat_scope function_scope _ _]
 foo = 
 fix foo (A : Type) (l : list A) {struct l} : option A :=
   match l with
@@ -48,9 +50,25 @@ f =
 fun H : B =>
 match H with
 | AC x =>
-    (let b0 := b in
-     if b0 as b return (P b -> True)
+    let b0 := b in
+    (if b0 as b return (P b -> True)
      then fun _ : P true => Logic.I
      else fun _ : P false => Logic.I) x
 end
      : B -> True
+The command has indeed failed with message:
+Non exhaustive pattern-matching: no clause found for pattern 
+gadtTy _ _
+The command has indeed failed with message:
+In environment
+texpDenote : forall t : type, texp t -> typeDenote t
+t : type
+e : texp t
+t1 : type
+t2 : type
+t0 : type
+b : tbinop t1 t2 t0
+e1 : texp t1
+e2 : texp t2
+The term "0" has type "nat" while it is expected to have type
+ "typeDenote t0".
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 4116a5eb..40748964 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -66,14 +66,43 @@ Print foo'.
 (* Was bug #3293 (eta-expansion at "match" printing time was failing because
    of let-in's interpreted as being part of the expansion)  *)
 
-Variable b : bool.
-Variable P : bool -> Prop.
+Axiom b : bool.
+Axiom P : bool -> Prop.
 Inductive B : Prop := AC : P b -> B.
 Definition f : B -> True.
 
 Proof.
-intros [].
-destruct b as [|] ; intros _ ; exact Logic.I.
+intros [x].
+destruct b as [|] ; exact Logic.I.
 Defined.
 
 Print f.
+
+(* Was enhancement request #5142 (error message reported on the most
+   general return clause heuristic) *)
+
+Inductive gadt : Type -> Type :=
+| gadtNat : nat -> gadt nat
+| gadtTy : forall T, T -> gadt T.
+
+Fail Definition gadt_id T (x: gadt T) : gadt T :=
+  match x with
+  | gadtNat n => gadtNat n
+  end.
+
+(* A variant of #5142 (see Satrajit Roy's example on coq-club (Oct 17, 2016)) *)
+
+Inductive type:Set:=Nat.
+Inductive tbinop:type->type->type->Set:= TPlus : tbinop Nat Nat Nat.
+Inductive texp:type->Set:=
+ |TNConst:nat->texp Nat
+ |TBinop:forall t1 t2 t, tbinop t1 t2 t->texp t1->texp t2->texp t.
+Definition typeDenote(t:type):Set:= match t with Nat => nat end.
+
+(* We expect a failure on TBinop *)
+Fail Fixpoint texpDenote t (e:texp t):typeDenote t:=
+  match e with
+  | TNConst n => n
+  | TBinop t1 t2 _ b e1 e2 => O
+  end.
+
diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out
index 6354ad46..06a6b2d1 100644
--- a/test-suite/output/Errors.out
+++ b/test-suite/output/Errors.out
@@ -5,3 +5,6 @@ Unable to unify "nat" with "True".
 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 ( (ident) := (lglob) )" failed.
+Error: Instance is not well-typed in the environment of ?x.
diff --git a/test-suite/output/Errors.v b/test-suite/output/Errors.v
index 352c8738..424d2480 100644
--- a/test-suite/output/Errors.v
+++ b/test-suite/output/Errors.v
@@ -16,3 +16,12 @@ Goal True.
 Fail simpl; apply 0.
 Fail simpl; f 0.
 Abort.
+
+(* Test instantiate error messages *)
+
+Goal forall T1 (P1 : T1 -> Type), sigT P1 -> sigT P1.
+intros T1 P1 H1.
+eexists ?[x].
+destruct H1 as [x1 H1].
+Fail instantiate (x:=projT1 x1).
+Abort.
diff --git a/test-suite/output/Existentials.out b/test-suite/output/Existentials.out
index 52e1e0ed..9680d2bb 100644
--- a/test-suite/output/Existentials.out
+++ b/test-suite/output/Existentials.out
@@ -1,5 +1,4 @@
-Existential 1 =
-?Goal1 : [p : nat  q := S p : nat  n : nat  m : nat |- ?y = m] 
+Existential 1 = ?Goal : [p : nat  q := S p : nat  n : nat  m : nat |- ?y = m] 
 Existential 2 =
 ?y : [p : nat  q := S p : nat  n : nat  m : nat |- nat] (p, q cannot be used)
 Existential 3 = ?Goal0 : [q : nat  n : nat  m : nat |- n = ?y] 
diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out
index bbfd3405..c17c63e7 100644
--- a/test-suite/output/InitSyntax.out
+++ b/test-suite/output/InitSyntax.out
@@ -4,7 +4,8 @@ Inductive sig2 (A : Type) (P Q : A -> Prop) : Type :=
 For sig2: Argument A is implicit
 For exist2: Argument A is implicit
 For sig2: Argument scopes are [type_scope type_scope type_scope]
-For exist2: Argument scopes are [type_scope _ _ _ _ _]
+For exist2: Argument scopes are [type_scope function_scope function_scope _ _
+              _]
 exists x : nat, x = x
      : Prop
 fun b : bool => if b then b else b
diff --git a/test-suite/output/Intuition.out b/test-suite/output/Intuition.out
index e99d9fde..f2bf25ca 100644
--- a/test-suite/output/Intuition.out
+++ b/test-suite/output/Intuition.out
@@ -3,4 +3,4 @@
   m, n : Z
   H : (m >= n)%Z
   ============================
-   (m >= m)%Z
+  (m >= m)%Z
diff --git a/test-suite/output/Naming.out b/test-suite/output/Naming.out
index f0d2562e..c142d28e 100644
--- a/test-suite/output/Naming.out
+++ b/test-suite/output/Naming.out
@@ -2,40 +2,40 @@
   
   x3 : nat
   ============================
-   forall x x1 x4 x0 : nat,
-   (forall x2 x5 : nat, x2 + x1 = x4 + x5) -> x + x1 = x4 + x0
+  forall x x1 x4 x0 : nat,
+  (forall x2 x5 : nat, x2 + x1 = x4 + x5) -> x + x1 = x4 + x0
 1 subgoal
   
   x3, x, x1, x4, x0 : nat
   H : forall x x3 : nat, x + x1 = x4 + x3
   ============================
-   x + x1 = x4 + x0
+  x + x1 = x4 + x0
 1 subgoal
   
   x3 : nat
   ============================
-   forall x x1 x4 x0 : nat,
-   (forall x2 x5 : nat, x2 + x1 = x4 + x5 -> foo (S x2 + x1)) ->
-   x + x1 = x4 + x0 -> foo (S x)
+  forall x x1 x4 x0 : nat,
+  (forall x2 x5 : nat, x2 + x1 = x4 + x5 -> foo (S x2 + x1)) ->
+  x + x1 = x4 + x0 -> foo (S x)
 1 subgoal
   
   x3 : nat
   ============================
-   forall x x1 x4 x0 : nat,
-   (forall x2 x5 : nat,
-    x2 + x1 = x4 + x5 ->
-    forall x6 x7 x8 S0 : nat, x6 + S0 = x7 + x8 + (S x2 + x1)) ->
-   x + x1 = x4 + x0 ->
-   forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
+  forall x x1 x4 x0 : nat,
+  (forall x2 x5 : nat,
+   x2 + x1 = x4 + x5 ->
+   forall x6 x7 x8 S0 : nat, x6 + S0 = x7 + x8 + (S x2 + x1)) ->
+  x + x1 = x4 + x0 ->
+  forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
 1 subgoal
   
   x3, x, x1, x4, x0 : nat
   ============================
-   (forall x2 x5 : nat,
-    x2 + x1 = x4 + x5 ->
-    forall x6 x7 x8 S0 : nat, x6 + S0 = x7 + x8 + (S x2 + x1)) ->
-   x + x1 = x4 + x0 ->
-   forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
+  (forall x2 x5 : nat,
+   x2 + x1 = x4 + x5 ->
+   forall x6 x7 x8 S0 : nat, x6 + S0 = x7 + x8 + (S x2 + x1)) ->
+  x + x1 = x4 + x0 ->
+  forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
 1 subgoal
   
   x3, x, x1, x4, x0 : nat
@@ -44,7 +44,7 @@
       forall x0 x4 x5 S0 : nat, x0 + S0 = x4 + x5 + (S x + x1)
   H0 : x + x1 = x4 + x0
   ============================
-   forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
+  forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
 1 subgoal
   
   x3, x, x1, x4, x0 : nat
@@ -54,10 +54,10 @@
   H0 : x + x1 = x4 + x0
   x5, x6, x7, S : nat
   ============================
-   x5 + S = x6 + x7 + Datatypes.S x
+  x5 + S = x6 + x7 + Datatypes.S x
 1 subgoal
   
   x3, a : nat
   H : a = 0 -> forall a : nat, a = 0
   ============================
-   a = 0
+  a = 0
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index b1558dab..26eaca82 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -111,14 +111,14 @@ fun x : option Z => match x with
                     | NONE2 => 0
                     end
      : option Z -> Z
-fun x : list ?T1 => match x with
-                    | NIL => NONE2
-                    | (_ :') t => SOME2 t
-                    end
-     : list ?T1 -> option (list ?T1)
+fun x : list ?T => match x with
+                   | NIL => NONE2
+                   | (_ :') t => SOME2 t
+                   end
+     : list ?T -> option (list ?T)
 where
-?T1 : [x : list ?T1  x1 : list ?T1  x0 := x1 : list ?T1 |- Type] (x, x1,
-      x0 cannot be used)
+?T : [x : list ?T  x1 : list ?T  x0 := x1 : list ?T |- Type] (x, x1,
+     x0 cannot be used)
 s
      : s
 10
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index adba688e..2ccca829 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -133,8 +133,7 @@ Fail Notation "( x , y , .. , z )" := (pair x (pair y z)).
 Fail Notation "( x , y , .. , z )" := (pair x .. (pair y w) ..).
 
 (* Right-unbound variable *)
-(* Now allowed with an only parsing restriction *)
-Notation "( x , y , .. , z )" := (pair y .. (pair z 0) ..).
+Notation "( x , y , .. , z )" := (pair y .. (pair z 0) ..) (only parsing).
 
 (* Not the right kind of recursive pattern *)
 Fail Notation "( x , y , .. , z )" := (ex (fun z => .. (ex (fun y => x)) ..)).
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index 58ec1de5..ad60aecc 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -12,7 +12,7 @@ let '(a, _, _) := (2, 3, 4) in a
      : nat
 exists myx y : bool, myx = y
      : Prop
-fun (P : nat -> nat -> Prop) (x : nat) => exists x0, P x x0
+fun (P : nat -> nat -> Prop) (x : nat) => exists y, P x y
      : (nat -> nat -> Prop) -> nat -> Prop
 ∃ n p : nat, n + p = 0
      : Prop
@@ -50,3 +50,37 @@ end
      : nat -> nat
 # _ : nat => 2
      : nat -> nat
+# x : nat => # H : x <= 0 => exist (le x) 0 H
+     : ∀ x : nat, x <= 0 -> {x0 : nat | x <= x0}
+exist (Q x) y conj
+     : {x0 : A | Q x x0}
+% i
+     : nat -> nat
+% j
+     : nat -> nat
+{1, 2}
+     : nat -> Prop
+a#
+     : Set
+a#
+     : Set
+a≡
+     : Set
+a≡
+     : Set
+.≡
+     : Set
+.≡
+     : Set
+.a#
+     : Set
+.a#
+     : Set
+.a≡
+     : Set
+.a≡
+     : Set
+.α
+     : Set
+.α
+     : Set
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index e53c94ef..ceb29d1b 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -68,6 +68,7 @@ Check let' f x y (a:=0) z (b:bool) := x+y+z+1 in f 0 1 2.
 
 (* In practice, only the printing rule is used here *)
 (* Note: does not work for pattern *)
+Module A.
 Notation "f ( x )" := (f x) (at level 10, format "f ( x )").
 Check fun f x => f x + S x.
 
@@ -77,6 +78,7 @@ Notation plus2 n := (S (S n)).
 (* plus2 was not correctly printed in the two following tests in 8.3pl1 *)
 Print plus2.
 Check fun n => match n with list1 => 0 | _ => 2 end.
+End A.
 
 (* This one is not fully satisfactory because binders in the same type
    are re-factorized and parentheses are needed even for atomic binder
@@ -98,3 +100,48 @@ Notation "#  x : T => t" := (fun x : T => t)
 
 Check # x : nat => x.
 Check # _ : nat => 2.
+
+(* Check bug 4677 *)
+Check fun x (H:le x 0) => exist (le x) 0 H.
+
+Parameters (A : Set) (x y : A) (Q : A -> A -> Prop) (conj : Q x y).
+Check (exist (Q x) y conj).
+
+(* Check bug #4854 *)
+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}).
+
+(**********************************************************************)
+(* Check notations of the form ".a", ".a≡", "a≡"                      *)
+(* Only "a#", "a≡" and ".≡" were working properly for parsing. The    *)
+(* other ones were working only for printing.                         *)
+
+Notation "a#" := nat.
+Check nat.
+Check a#.
+
+Notation "a≡" := nat.
+Check nat.
+Check a≡.
+
+Notation ".≡" := nat.
+Check nat.
+Check .≡.
+
+Notation ".a#" := nat.
+Check nat.
+Check .a#.
+
+Notation ".a≡" := nat.
+Check nat.
+Check .a≡.
+
+Notation ".α" := nat.
+Check nat.
+Check .α.
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
new file mode 100644
index 00000000..360f3796
--- /dev/null
+++ b/test-suite/output/Notations3.out
@@ -0,0 +1,100 @@
+[<0, 2 >]
+     : nat * nat * (nat * nat)
+[<0, 2 >]
+     : nat * nat * (nat * nat)
+(0, 2, (2, 2))
+     : nat * nat * (nat * nat)
+pair (pair O (S (S O))) (pair (S (S O)) O)
+     : prod (prod nat nat) (prod nat nat)
+<< 0, 2, 4 >>
+     : nat * nat * nat * (nat * (nat * nat))
+<< 0, 2, 4 >>
+     : nat * nat * nat * (nat * (nat * nat))
+(0, 2, 4, (2, (2, 0)))
+     : nat * nat * nat * (nat * (nat * nat))
+(0, 2, 4, (0, (2, 4)))
+     : nat * nat * nat * (nat * (nat * nat))
+pair (pair (pair O (S (S O))) (S (S (S (S O)))))
+  (pair (S (S (S (S O)))) (pair (S (S O)) O))
+     : prod (prod (prod nat nat) nat) (prod nat (prod nat nat))
+ETA x y : nat, Nat.add
+     : nat -> nat -> nat
+ETA x y : nat, Nat.add
+     : nat -> nat -> nat
+ETA x y : nat, Nat.add
+     : nat -> nat -> nat
+fun x y : nat => Nat.add x y
+     : forall (_ : nat) (_ : nat), nat
+ETA x y : nat, le_S
+     : forall x y : nat, x <= y -> x <= S y
+fun f : forall x : nat * (bool * unit), ?T => CURRY (x : nat) (y : bool), f
+     : (forall x : nat * (bool * unit), ?T) ->
+       forall (x : nat) (y : bool), ?T@{x:=(x, (y, tt))}
+where
+?T : [x : nat * (bool * unit) |- Type] 
+fun f : forall x : bool * (nat * unit), ?T =>
+CURRYINV (x : nat) (y : bool), f
+     : (forall x : bool * (nat * unit), ?T) ->
+       forall (x : nat) (y : bool), ?T@{x:=(y, (x, tt))}
+where
+?T : [x : bool * (nat * unit) |- Type] 
+fun f : forall x : unit * nat * bool, ?T => CURRYLEFT (x : nat) (y : bool), f
+     : (forall x : unit * nat * bool, ?T) ->
+       forall (x : nat) (y : bool), ?T@{x:=(tt, x, y)}
+where
+?T : [x : unit * nat * bool |- Type] 
+fun f : forall x : unit * bool * nat, ?T =>
+CURRYINVLEFT (x : nat) (y : bool), f
+     : (forall x : unit * bool * nat, ?T) ->
+       forall (x : nat) (y : bool), ?T@{x:=(tt, y, x)}
+where
+?T : [x : unit * bool * nat |- Type] 
+forall n : nat, {#n | 1 > n}
+     : Prop
+forall x : nat, {|x | x > 0|}
+     : Prop
+exists2 x : nat, x = 1 & x = 2
+     : Prop
+fun n : nat =>
+foo2 n (fun x y z : nat => (fun _ _ _ : nat => x + y + z = 0) z y x)
+     : nat -> Prop
+fun n : nat =>
+foo2 n (fun a b c : nat => (fun _ _ _ : nat => a + b + c = 0) c b a)
+     : nat -> Prop
+fun n : nat =>
+foo2 n (fun n0 y z : nat => (fun _ _ _ : nat => n0 + y + z = 0) z y n0)
+     : nat -> Prop
+fun n : nat =>
+foo2 n (fun x n0 z : nat => (fun _ _ _ : nat => x + n0 + z = 0) z n0 x)
+     : nat -> Prop
+fun n : nat =>
+foo2 n (fun x y n0 : nat => (fun _ _ _ : nat => x + y + n0 = 0) n0 y x)
+     : nat -> Prop
+fun n : nat => {|n, y | fun _ _ _ : nat => n + y = 0 |}_2
+     : nat -> Prop
+fun n : nat => {|n, y | fun _ _ _ : nat => n + y = 0 |}_2
+     : nat -> Prop
+fun n : nat => {|n, n0 | fun _ _ _ : nat => n + n0 = 0 |}_2
+     : nat -> Prop
+fun n : nat =>
+foo2 n (fun x y z : nat => (fun _ _ _ : nat => x + y + n = 0) z y x)
+     : nat -> Prop
+fun n : nat =>
+foo2 n (fun x y z : nat => (fun _ _ _ : nat => x + y + n = 0) z y x)
+     : nat -> Prop
+fun n : nat => {|n, fun _ : nat => 0 = 0 |}_3
+     : nat -> Prop
+fun n : nat => {|n, fun _ : nat => n = 0 |}_3
+     : nat -> Prop
+fun n : nat => foo3 n (fun x _ : nat => ETA z : nat, (fun _ : nat => x = 0))
+     : nat -> Prop
+fun n : nat => {|n, fun _ : nat => 0 = 0 |}_4
+     : nat -> Prop
+fun n : nat => {|n, fun _ : nat => n = 0 |}_4
+     : nat -> Prop
+fun n : nat => foo4 n (fun _ _ : nat => ETA z : nat, (fun _ : nat => z = 0))
+     : nat -> Prop
+fun n : nat => foo4 n (fun _ y : nat => ETA z : nat, (fun _ : nat => y = 0))
+     : nat -> Prop
+tele (t : Type) '(y, z) (x : t0) := tt
+     : forall t : Type, nat * nat -> t -> fpack
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
new file mode 100644
index 00000000..4b8bfe31
--- /dev/null
+++ b/test-suite/output/Notations3.v
@@ -0,0 +1,141 @@
+(**********************************************************************)
+(* Check printing of notations with several instances of a recursive pattern *)
+(* Was wrong but I could not trigger a problem due to the collision between *)
+(* different instances of ".." *)
+
+Notation "[< x , y , .. , z >]" := (pair (.. (pair x y) ..) z,pair y ( .. (pair z x) ..)).
+Check [<0,2>].
+Check ((0,2),(2,0)).
+Check ((0,2),(2,2)).
+Unset Printing Notations.
+Check [<0,2>].
+Set Printing Notations.
+
+Notation "<< x , y , .. , z >>" := ((.. (x,y) .., z),(z, .. (y,x) ..)).
+Check <<0,2,4>>.
+Check (((0,2),4),(4,(2,0))).
+Check (((0,2),4),(2,(2,0))).
+Check (((0,2),4),(0,(2,4))).
+Unset Printing Notations.
+Check <<0,2,4>>.
+Set Printing Notations.
+
+(**********************************************************************)
+(* Check notations with recursive notations both in binders and terms *)
+
+Notation "'ETA' x .. y , f" :=
+  (fun x => .. (fun y => (.. (f x) ..) y ) ..)
+  (at level 200, x binder, y binder).
+Check ETA (x:nat) (y:nat), Nat.add.
+Check ETA (x y:nat), Nat.add.
+Check ETA x y, Nat.add.
+Unset Printing Notations.
+Check ETA (x:nat) (y:nat), Nat.add.
+Set Printing Notations.
+Check ETA x y, le_S.
+
+Notation "'CURRY' x .. y , f" := (fun x => .. (fun y => f (x, .. (y,tt) ..)) ..)
+  (at level 200, x binder, y binder).
+Check fun f => CURRY (x:nat) (y:bool), f.
+
+Notation "'CURRYINV' x .. y , f" := (fun x => .. (fun y => f (y, .. (x,tt) ..)) ..)
+  (at level 200, x binder, y binder).
+Check fun f => CURRYINV (x:nat) (y:bool), f.
+
+Notation "'CURRYLEFT' x .. y , f" := (fun x => .. (fun y => f (.. (tt,x) .., y)) ..)
+  (at level 200, x binder, y binder).
+Check fun f => CURRYLEFT (x:nat) (y:bool), f.
+
+Notation "'CURRYINVLEFT' x .. y , f" := (fun x => .. (fun y => f (.. (tt,y) .., x)) ..)
+  (at level 200, x binder, y binder).
+Check fun f => CURRYINVLEFT (x:nat) (y:bool), f.
+
+(**********************************************************************)
+(* Notations with variables bound both as a term and as a binder      *)
+(* This is #4592 *)
+
+Notation "{# x | P }" := (ex2 (fun y => x = y) (fun x => P)).
+Check forall n:nat, {# n | 1 > n}.
+
+Parameter foo : forall {T}(x : T)(P : T -> Prop), Prop.
+Notation "{| x | P |}" := (foo x (fun x => P)).
+Check forall x:nat, {| x | x > 0 |}.
+
+Check ex2 (fun x => x=1) (fun x0 => x0=2).
+
+(* Other tests about alpha-conversions: the following notation
+   contains all three kinds of bindings:
+
+   - x is bound in the lhs as a term and a binder: its name is forced
+     by its position as a term; it can bind variables in P
+   - y is bound in the lhs as a binder only: its name is given by its
+     name as a binder in the term to display; it can bind variables in P
+   - z is a binder local to the rhs; it cannot bind a variable in P
+*)
+
+Parameter foo2 : forall {T}(x : T)(P : T -> T -> T -> Prop), Prop.
+Notation "{| x , y | P |}_2" := (foo2 x (fun x y z => P z y x)).
+
+(* Not printable: z (resp c, n) occurs in P *)
+Check fun n => foo2 n (fun x y z => (fun _ _ _ => x+y+z=0) z y x).
+Check fun n => foo2 n (fun a b c => (fun _ _ _ => a+b+c=0) c b a).
+Check fun n => foo2 n (fun n y z => (fun _ _ _ => n+y+z=0) z y n).
+Check fun n => foo2 n (fun x n z => (fun _ _ _ => x+n+z=0) z n x).
+Check fun n => foo2 n (fun x y n => (fun _ _ _ => x+y+n=0) n y x).
+
+(* Printable *)
+Check fun n => foo2 n (fun x y z => (fun _ _ _ => x+y=0) z y x).
+Check fun n => foo2 n (fun n y z => (fun _ _ _ => n+y=0) z y n).
+Check fun n => foo2 n (fun x n z => (fun _ _ _ => x+n=0) z n x).
+
+(* Not printable: renaming x into n would bind the 2nd occurrence of n *)
+Check fun n => foo2 n (fun x y z => (fun _ _ _ => x+y+n=0) z y x).
+Check fun n => foo2 n (fun x y z => (fun _ _ _ => x+y+n=0) z y x).
+
+(* Other tests *)
+Parameter foo3 : forall {T}(x : T)(P : T -> T -> T -> Prop), Prop.
+Notation "{| x , P |}_3" := (foo3 x (fun x x x => P x)).
+
+(* Printable *)
+Check fun n : nat => foo3 n (fun x y z => (fun _ => 0=0) z).
+Check fun n => foo3 n (fun x y z => (fun _ => z=0) z).
+
+(* Not printable: renaming z in n would hide the renaming of x into n *)
+Check fun n => foo3 n (fun x y z => (fun _ => x=0) z).
+
+(* Other tests *)
+Parameter foo4 : forall {T}(x : T)(P : T -> T -> T -> Prop), Prop.
+Notation "{| x , P |}_4" := (foo4 x (fun x _ z => P z)).
+
+(* Printable *)
+Check fun n : nat => foo4 n (fun x y z => (fun _ => 0=0) z).
+Check fun n => foo4 n (fun x y z => (fun _ => x=0) z).
+
+(* Not printable: y, z not allowed to occur in P *)
+Check fun n => foo4 n (fun x y z => (fun _ => z=0) z).
+Check fun n => foo4 n (fun x y z => (fun _ => y=0) z).
+
+(**********************************************************************)
+(* Test printing of #4932                                             *)
+
+Inductive ftele : Type :=
+| fb {T:Type} : T -> ftele
+| fr {T} : (T -> ftele) -> ftele.
+
+Fixpoint args ftele : Type :=
+  match ftele with
+    | fb _ => unit
+    | fr f => sigT (fun t => args (f t))
+  end.
+
+Definition fpack := sigT args.
+Definition pack fp fa : fpack := existT _ fp fa.
+
+Notation "'tele' x .. z := b" :=
+  (fun x => .. (fun z =>
+     pack (fr (fun x => .. ( fr (fun z => fb b) ) .. ) )
+          (existT _ x .. (existT _ z tt) .. )
+                ) ..)
+  (at level 85, x binder, z binder).
+
+Check tele (t:Type) '((y,z):nat*nat) (x:t) := tt.
diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out
new file mode 100644
index 00000000..c012a86b
--- /dev/null
+++ b/test-suite/output/PatternsInBinders.out
@@ -0,0 +1,39 @@
+swap = fun '(x, y) => (y, x)
+     : A * B -> B * A
+fun '(x, y) => (y, x)
+     : A * B -> B * A
+forall '(x, y), swap (x, y) = (y, x)
+     : Prop
+proj_informative = fun '(exist _ x _) => x : A
+     : {x : A | P x} -> A
+foo = fun '(Bar n b tt p) => if b then n + p else n - p
+     : Foo -> nat
+baz = 
+fun '(Bar n1 _ tt p1) '(Bar _ _ tt _) => n1 + p1
+     : Foo -> Foo -> nat
+swap = 
+fun (A B : Type) '(x, y) => (y, x)
+     : forall A B : Type, A * B -> B * A
+
+Arguments A, B are implicit and maximally inserted
+Argument scopes are [type_scope type_scope _]
+fun (A B : Type) '(x, y) => swap (x, y) = (y, x)
+     : forall A B : Type, A * B -> Prop
+forall (A B : Type) '(x, y), swap (x, y) = (y, x)
+     : Prop
+exists '(x, y), swap (x, y) = (y, x)
+     : Prop
+exists '(x, y) '(z, w), swap (x, y) = (z, w)
+     : Prop
+λ '(x, y), (y, x)
+     : A * B → B * A
+∀ '(x, y), swap (x, y) = (y, x)
+     : Prop
+both_z = 
+fun pat : nat * nat =>
+let '(n, p) as pat0 := pat return (F pat0) in (Z n, Z p) : F (n, p)
+     : forall pat : nat * nat, F pat
+fun '(x, y) '(z, t) => swap (x, y) = (z, t)
+     : A * B -> B * A -> Prop
+forall '(x, y) '(z, t), swap (x, y) = (z, t)
+     : Prop
diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v
new file mode 100644
index 00000000..6fa357a9
--- /dev/null
+++ b/test-suite/output/PatternsInBinders.v
@@ -0,0 +1,66 @@
+Require Coq.Unicode.Utf8.
+
+(** The purpose of this file is to test printing of the destructive
+    patterns used in binders ([fun] and [forall]). *)
+
+Parameters (A B : Type) (P:A->Prop).
+
+Definition swap '((x,y) : A*B) := (y,x).
+Print swap.
+
+Check fun '((x,y) : A*B) => (y,x).
+
+Check forall '(x,y), swap (x,y) = (y,x).
+
+Definition proj_informative '(exist _ x _ : { x:A | P x }) : A := x.
+Print proj_informative.
+
+Inductive Foo := Bar : nat -> bool -> unit -> nat -> Foo.
+Definition foo '(Bar n b tt p) :=
+  if b then n+p else n-p.
+Print foo.
+
+Definition baz '(Bar n1 b1 tt p1) '(Bar n2 b2 tt p2) := n1+p1.
+Print baz.
+
+Module WithParameters.
+
+Definition swap {A B} '((x,y) : A*B) := (y,x).
+Print swap.
+
+Check fun (A B:Type) '((x,y) : A*B) => swap (x,y) = (y,x).
+Check forall (A B:Type) '((x,y) : A*B), swap (x,y) = (y,x).
+
+Check exists '((x,y):A*A), swap (x,y) = (y,x).
+Check exists '((x,y):A*A) '(z,w), swap (x,y) = (z,w).
+
+End WithParameters.
+
+(** Some test involving unicode notations. *)
+Module WithUnicode.
+
+  Import Coq.Unicode.Utf8.
+
+  Check λ '((x,y) : A*B),  (y,x).
+  Check ∀ '(x,y), swap (x,y) = (y,x).
+
+End WithUnicode.
+
+(** * Suboptimal printing *)
+
+Module Suboptimal.
+
+(** This test shows an example which exposes the [let] introduced by
+    the pattern notation in binders. *)
+
+Inductive Fin (n:nat) := Z : Fin n.
+Definition F '(n,p) : Type := (Fin n * Fin p)%type.
+Definition both_z '(n,p) : F (n,p) := (Z _,Z _).
+Print both_z.
+
+(** Test factorization of binders *)
+
+Check fun '((x,y) : A*B) '(z,t) => swap (x,y) = (z,t).
+Check forall '(x,y) '((z,t) : B*A), swap (x,y) = (z,t).
+
+End Suboptimal.
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out
index ba076f05..1307a8f2 100644
--- a/test-suite/output/PrintInfos.out
+++ b/test-suite/output/PrintInfos.out
@@ -2,7 +2,7 @@ existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x}
 
 existT is template universe polymorphic
 Argument A is implicit
-Argument scopes are [type_scope _ _ _]
+Argument scopes are [type_scope function_scope _ _]
 Expands to: Constructor Coq.Init.Specif.existT
 Inductive sigT (A : Type) (P : A -> Type) : Type :=
     existT : forall x : A, P x -> {x : A & P x}
@@ -10,7 +10,7 @@ Inductive sigT (A : Type) (P : A -> Type) : Type :=
 For sigT: Argument A is implicit
 For existT: Argument A is implicit
 For sigT: Argument scopes are [type_scope type_scope]
-For existT: Argument scopes are [type_scope _ _ _]
+For existT: Argument scopes are [type_scope function_scope _ _]
 existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x}
 
 Argument A is implicit
@@ -66,14 +66,6 @@ For le_S: Argument n is implicit and maximally inserted
 For le: Argument scopes are [nat_scope nat_scope]
 For le_n: Argument scope is [nat_scope]
 For le_S: Argument scopes are [nat_scope nat_scope _]
-Inductive le (n : nat) : nat -> Prop :=
-    le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m
-
-For le_S: Argument m is implicit
-For le_S: Argument n is implicit and maximally inserted
-For le: Argument scopes are [nat_scope nat_scope]
-For le_n: Argument scope is [nat_scope]
-For le_S: Argument scopes are [nat_scope nat_scope _]
 comparison : Set
 
 Expands to: Inductive Coq.Init.Datatypes.comparison
@@ -92,19 +84,6 @@ Expanded type for implicit arguments
 bar : forall x : nat, x = 0
 
 Argument x is implicit and maximally inserted
-bar : foo
-
-Expanded type for implicit arguments
-bar : forall x : nat, x = 0
-
-Argument x is implicit and maximally inserted
-Expands to: Constant Top.bar
-*** [ bar : foo ]
-
-Expanded type for implicit arguments
-bar : forall x : nat, x = 0
-
-Argument x is implicit and maximally inserted
 Module Coq.Init.Peano
 Notation existS2 := existT2
 Expands to: Notation Coq.Init.Specif.existS2
@@ -117,15 +96,6 @@ For eq_refl, when applied to 1 argument:
   Argument A is implicit and maximally inserted
 For eq: Argument scopes are [type_scope _ _]
 For eq_refl: Argument scopes are [type_scope _]
-Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
-
-For eq: Argument A is implicit and maximally inserted
-For eq_refl, when applied to no arguments:
-  Arguments A, x are implicit and maximally inserted
-For eq_refl, when applied to 1 argument:
-  Argument A is implicit and maximally inserted
-For eq: Argument scopes are [type_scope _ _]
-For eq_refl: Argument scopes are [type_scope _]
 n:nat
 
 Hypothesis of the goal context.
diff --git a/test-suite/output/PrintInfos.v b/test-suite/output/PrintInfos.v
index 3c623346..08918981 100644
--- a/test-suite/output/PrintInfos.v
+++ b/test-suite/output/PrintInfos.v
@@ -12,10 +12,7 @@ Print Implicit Nat.add.
 
 About plus_n_O.
 
-Implicit Arguments le_S [[n] m].
-Print le_S.
-
-Arguments le_S {n} [m] _. (* Test new syntax *)
+Arguments le_S {n} [m] _.
 Print le_S.
 
 About comparison.
@@ -23,21 +20,15 @@ Print comparison.
 
 Definition foo := forall x, x = 0.
 Parameter bar : foo.
-Implicit Arguments bar [x].
-About bar.
-Print bar.
 
-Arguments bar [x]. (* Test new syntax *)
+Arguments bar [x].
 About bar.
 Print bar.
 
 About Peano. (* Module *)
 About existS2. (* Notation *)
 
-Implicit Arguments eq_refl [[A] [x]] [[A]].
-Print eq_refl.
-
-Arguments eq_refl {A} {x}, {A} x. (* Test new syntax *)
+Arguments eq_refl {A} {x}, {A} x.
 Print eq_refl.
 
 
diff --git a/test-suite/output/PrintModule.out b/test-suite/output/PrintModule.out
index db464fd0..751d5fcc 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 999d9a98..5f30f7cd 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/Quote.out b/test-suite/output/Quote.out
index ca7fc362..998eb37c 100644
--- a/test-suite/output/Quote.out
+++ b/test-suite/output/Quote.out
@@ -8,17 +8,17 @@
   H : interp_f (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (f_atom End_idx) \/
       B
   ============================
-   interp_f
-     (Node_vm B (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (Empty_vm Prop))
-     (f_and (f_atom (Left_idx End_idx))
-        (f_and (f_or (f_atom End_idx) (f_atom (Left_idx End_idx)))
-           (f_or (f_atom (Left_idx End_idx)) (f_not (f_atom End_idx)))))
+  interp_f
+    (Node_vm B (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (Empty_vm Prop))
+    (f_and (f_atom (Left_idx End_idx))
+       (f_and (f_or (f_atom End_idx) (f_atom (Left_idx End_idx)))
+          (f_or (f_atom (Left_idx End_idx)) (f_not (f_atom End_idx)))))
 1 subgoal
   
   H : interp_f (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (f_atom End_idx) \/
       B
   ============================
-   interp_f (Node_vm B (Empty_vm Prop) (Empty_vm Prop))
-     (f_and (f_const A)
-        (f_and (f_or (f_atom End_idx) (f_const A))
-           (f_or (f_const A) (f_not (f_atom End_idx)))))
+  interp_f (Node_vm B (Empty_vm Prop) (Empty_vm Prop))
+    (f_and (f_const A)
+       (f_and (f_or (f_atom End_idx) (f_const A))
+          (f_or (f_const A) (f_not (f_atom End_idx)))))
diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out
index 1eb7eca8..f3c12eff 100644
--- a/test-suite/output/SearchPattern.out
+++ b/test-suite/output/SearchPattern.out
@@ -40,7 +40,6 @@ Nat.land: nat -> nat -> nat
 Nat.lor: nat -> nat -> nat
 Nat.ldiff: nat -> nat -> nat
 Nat.lxor: nat -> nat -> nat
-
 S: nat -> nat
 Nat.succ: nat -> nat
 Nat.pred: nat -> nat
@@ -74,7 +73,6 @@ le_n: forall n : nat, n <= n
 pair: forall A B : Type, A -> B -> A * B
 conj: forall A B : Prop, A -> B -> A /\ B
 Nat.divmod: nat -> nat -> nat -> nat -> nat * nat
-
 h: n <> newdef n
 h: n <> newdef n
 h: P n
diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out
index 9949658c..239edd1d 100644
--- a/test-suite/output/Tactics.out
+++ b/test-suite/output/Tactics.out
@@ -1,4 +1,4 @@
 Ltac f H := split; [ a H | e H ]
 Ltac g := match goal with
-          | |- context [if ?X then _ else _] => case X
+          | |- context [ if ?X then _ else _ ] => case X
           end
diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out
index f2d14477..576fbd7c 100644
--- a/test-suite/output/inference.out
+++ b/test-suite/output/inference.out
@@ -6,13 +6,13 @@ fun e : option L => match e with
      : option L -> option L
 fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H
      : forall m n p : nat, S m <= S n + p -> m <= n + p
-fun n : nat => let x := A n in ?y ?y0 : T n
+fun n : nat => let x := A n : T n in ?y ?y0 : T n
      : forall n : nat, T n
 where
-?y : [n : nat  x := A n : T n |- ?T0 -> T n] 
-?y0 : [n : nat  x := A n : T n |- ?T0] 
+?y : [n : nat  x := A n : T n |- ?T -> T n] 
+?y0 : [n : nat  x := A n : T n |- ?T] 
 fun n : nat => ?y ?y0 : T n
      : forall n : nat, T n
 where
-?y : [n : nat |- ?T0 -> T n] 
-?y0 : [n : nat |- ?T0] 
+?y : [n : nat |- ?T -> T n] 
+?y0 : [n : nat |- ?T] 
diff --git a/test-suite/output/inference.v b/test-suite/output/inference.v
index cd9a4a12..1825db16 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 d003c70d..1ff09e3a 100644
--- a/test-suite/output/ltac.out
+++ b/test-suite/output/ltac.out
@@ -1,2 +1,34 @@
 The command has indeed failed with message:
-Error: Ltac variable y depends on pattern variable name z which is not bound in current context.
+Error:
+Ltac variable y depends on pattern variable name z which is not bound in current context.
+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 (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 (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 (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 (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 (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 (destruction_arg)", last call
+failed.
+Error: No primitive equality found.
+Hx
+nat
+nat
+0
+0
diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v
index 7e2610c7..76c37625 100644
--- a/test-suite/output/ltac.v
+++ b/test-suite/output/ltac.v
@@ -15,3 +15,45 @@ lazymatch goal with
 | H1 : HT |- _ => idtac
 end.
 Abort.
+
+Ltac f x y z :=
+  symmetry in x, y;
+  auto with z;
+  auto;
+  intros;
+  clearbody x;
+  generalize dependent z.
+
+Print Ltac f.
+
+(* Error messages *)
+
+Ltac g1 x := refine x.
+Tactic Notation "g2" constr(x) := g1 x.
+Tactic Notation "f1" constr(x) := refine x.
+Ltac f2 x := f1 x.
+Goal False.
+Fail g1 I.
+Fail f1 I.
+Fail g2 I.
+Fail f2 I.
+
+Ltac h x := injection x.
+Goal True -> False.
+Fail h I.
+intro H.
+Fail h H.
+
+(* Check printing of the "var" argument "Hx" *)
+Ltac m H := idtac H; exact H.
+Goal True.
+let a:=constr:(let Hx := 0 in ltac:(m Hx)) in idtac.
+
+(* Check consistency of interpretation scopes (#4398) *)
+
+Goal nat*(0*0=0) -> nat*(0*0=0). intro.
+match goal with H: ?x*?y |- _ => idtac x end.
+match goal with |- ?x*?y => idtac x end.
+match goal with H: context [?x*?y] |- _ => idtac x end.
+match goal with |- context [?x*?y] => idtac x end.
+Abort.
diff --git a/test-suite/output/onlyprinting.out b/test-suite/output/onlyprinting.out
new file mode 100644
index 00000000..e0a30fcf
--- /dev/null
+++ b/test-suite/output/onlyprinting.out
@@ -0,0 +1,2 @@
+0:-) 0
+     : nat
diff --git a/test-suite/output/onlyprinting.v b/test-suite/output/onlyprinting.v
new file mode 100644
index 00000000..1973385a
--- /dev/null
+++ b/test-suite/output/onlyprinting.v
@@ -0,0 +1,5 @@
+Reserved Notation "x :-) y" (at level 50, only printing).
+
+Notation "x :-) y" := (plus x y).
+
+Check 0 + 0.
diff --git a/test-suite/output/qualification.out b/test-suite/output/qualification.out
new file mode 100644
index 00000000..9300c3f5
--- /dev/null
+++ b/test-suite/output/qualification.out
@@ -0,0 +1,3 @@
+File "stdin", line 19, characters 0-7:
+Error: Signature components for label test do not match: expected type
+"Top.M2.t = Top.M2.M.t" but found type "Top.M2.t = Top.M2.t".
diff --git a/test-suite/output/qualification.v b/test-suite/output/qualification.v
new file mode 100644
index 00000000..d39097e2
--- /dev/null
+++ b/test-suite/output/qualification.v
@@ -0,0 +1,19 @@
+Module Type T1.
+  Parameter t : Type.
+End T1.
+
+Module Type T2.
+  Declare Module M : T1.
+  Parameter t : Type.
+  Parameter test : t = M.t.
+End T2.
+
+Module M1 <: T1.
+  Definition t : Type := bool.
+End M1.
+
+Module M2 <: T2.
+  Module M := M1.
+  Definition t : Type := nat.
+  Lemma test : t = t. Proof. reflexivity. Qed.
+End M2.
diff --git a/test-suite/output/set.out b/test-suite/output/set.out
index 4dfd2bc2..4b72d73e 100644
--- a/test-suite/output/set.out
+++ b/test-suite/output/set.out
@@ -3,16 +3,16 @@
   y1 := 0 : nat
   x := 0 + 0 : nat
   ============================
-   x = x
+  x = x
 1 subgoal
   
   y1, y2 := 0 : nat
   x := y2 + 0 : nat
   ============================
-   x = x
+  x = x
 1 subgoal
   
   y1, y2, y3 := 0 : nat
   x := y2 + y3 : nat
   ============================
-   x = x
+  x = x
diff --git a/test-suite/output/simpl.out b/test-suite/output/simpl.out
index 73888da9..526e468f 100644
--- a/test-suite/output/simpl.out
+++ b/test-suite/output/simpl.out
@@ -2,14 +2,14 @@
   
   x : nat
   ============================
-   x = S x
+  x = S x
 1 subgoal
   
   x : nat
   ============================
-   0 + x = S x
+  0 + x = S x
 1 subgoal
   
   x : nat
   ============================
-   x = 1 + x
+  x = 1 + x
diff --git a/test-suite/output/subst.out b/test-suite/output/subst.out
new file mode 100644
index 00000000..209b2bc2
--- /dev/null
+++ b/test-suite/output/subst.out
@@ -0,0 +1,97 @@
+1 subgoal
+  
+  y, z : nat
+  Hy : y = 0
+  Hz : z = 0
+  H1 : 0 = 1
+  HA : True
+  H2 : 0 = 2
+  H3 : y = 3
+  HB : True
+  H4 : z = 4
+  ============================
+  True
+1 subgoal
+  
+  x, z : nat
+  Hx : x = 0
+  Hz : z = 0
+  H1 : x = 1
+  HA : True
+  H2 : x = 2
+  H3 : 0 = 3
+  HB : True
+  H4 : z = 4
+  ============================
+  True
+1 subgoal
+  
+  x, y : nat
+  Hx : x = 0
+  Hy : y = 0
+  H1 : x = 1
+  HA : True
+  H2 : x = 2
+  H3 : y = 3
+  HB : True
+  H4 : 0 = 4
+  ============================
+  True
+1 subgoal
+  
+  H1 : 0 = 1
+  HA : True
+  H2 : 0 = 2
+  H3 : 0 = 3
+  HB : True
+  H4 : 0 = 4
+  ============================
+  True
+1 subgoal
+  
+  y, z : nat
+  Hy : y = 0
+  Hz : z = 0
+  HA : True
+  H3 : y = 3
+  HB : True
+  H4 : z = 4
+  H1 : 0 = 1
+  H2 : 0 = 2
+  ============================
+  True
+1 subgoal
+  
+  x, z : nat
+  Hx : x = 0
+  Hz : z = 0
+  H1 : x = 1
+  HA : True
+  H2 : x = 2
+  HB : True
+  H4 : z = 4
+  H3 : 0 = 3
+  ============================
+  True
+1 subgoal
+  
+  x, y : nat
+  Hx : x = 0
+  Hy : y = 0
+  H1 : x = 1
+  HA : True
+  H2 : x = 2
+  H3 : y = 3
+  HB : True
+  H4 : 0 = 4
+  ============================
+  True
+1 subgoal
+  
+  HA, HB : True
+  H4 : 0 = 4
+  H3 : 0 = 3
+  H1 : 0 = 1
+  H2 : 0 = 2
+  ============================
+  True
diff --git a/test-suite/output/subst.v b/test-suite/output/subst.v
new file mode 100644
index 00000000..e48aa6bb
--- /dev/null
+++ b/test-suite/output/subst.v
@@ -0,0 +1,48 @@
+(* Ensure order of hypotheses is respected after "subst" *)
+
+Set Regular Subst Tactic.
+Goal forall x y z, x = 0 -> y = 0 -> z = 0 -> x = 1 -> True -> x = 2 -> y = 3 -> True -> z = 4 -> True.
+intros * Hx Hy Hz H1 HA H2 H3 HB H4.
+(* From now on, the order after subst is consistently H1, HA, H2, H3, HB, H4 *)
+subst x.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, H3, HB, H4, H1, H2 *)
+Show.
+Undo.
+subst y.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, HB, H4, H3 *)
+Show.
+Undo.
+subst z.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, H3, HB, H4 *)
+Show.
+Undo.
+subst.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, HB, H4, H3, H1, H2 *)
+(* In 8.5pl0 and 8.5pl1 with regular subst tactic mode, the order was HA, HB, H1, H2, H3, H4 *)
+Show.
+trivial.
+Qed.
+
+Unset Regular Subst Tactic.
+Goal forall x y z, x = 0 -> y = 0 -> z = 0 -> x = 1 -> True -> x = 2 -> y = 3 -> True -> z = 4 -> True.
+intros * Hx Hy Hz H1 HA H2 H3 HB H4.
+subst x.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, H3, HB, H4, H1, H2 *)
+Show.
+Undo.
+subst y.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, HB, H4, H3 *)
+Show.
+Undo.
+subst z.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, H3, HB, H4 *)
+Show.
+Undo.
+subst.
+(* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, HB, H4, H3, H1, H2 *)
+(* In 8.5pl0 and 8.5pl1 with regular subst tactic mode, the order was HA, HB, H1, H2, H3, H4 *)
+Show.
+trivial.
+Qed.
+
+
diff --git a/test-suite/output/unifconstraints.out b/test-suite/output/unifconstraints.out
new file mode 100644
index 00000000..ae846036
--- /dev/null
+++ b/test-suite/output/unifconstraints.out
@@ -0,0 +1,65 @@
+3 focused subgoals
+(shelved: 1)
+  
+  ============================
+  ?Goal 0
+
+subgoal 2 is:
+ forall n : nat, ?Goal n -> ?Goal (S n)
+subgoal 3 is:
+ nat
+unification constraint:
+ ?Goal ?Goal2 <=
+   True /\ True /\ True \/
+   veeryyyyyyyyyyyyloooooooooooooonggidentifier =
+   veeryyyyyyyyyyyyloooooooooooooonggidentifier
+3 focused subgoals
+(shelved: 1)
+  
+  n, m : nat
+  ============================
+  ?Goal@{n:=n; m:=m} 0
+
+subgoal 2 is:
+ forall n0 : nat, ?Goal@{n:=n; m:=m} n0 -> ?Goal@{n:=n; m:=m} (S n0)
+subgoal 3 is:
+ nat
+unification constraint:
+ ?Goal@{n:=n; m:=m} ?Goal2@{n:=n; m:=m} <=
+   True /\ True /\ True \/
+   veeryyyyyyyyyyyyloooooooooooooonggidentifier =
+   veeryyyyyyyyyyyyloooooooooooooonggidentifier
+3 focused subgoals
+(shelved: 1)
+  
+  m : nat
+  ============================
+  ?Goal1@{m:=m} 0
+
+subgoal 2 is:
+ forall n0 : nat, ?Goal1@{m:=m} n0 -> ?Goal1@{m:=m} (S n0)
+subgoal 3 is:
+ nat
+unification constraint:
+ 
+ n, m : nat |- ?Goal1@{m:=m} ?Goal0@{n:=n; m:=m} <=
+   True /\ True /\ True \/
+   veeryyyyyyyyyyyyloooooooooooooonggidentifier =
+   veeryyyyyyyyyyyyloooooooooooooonggidentifier
+3 focused subgoals
+(shelved: 1)
+  
+  m : nat
+  ============================
+  ?Goal0@{m:=m} 0
+
+subgoal 2 is:
+ forall n0 : nat, ?Goal0@{m:=m} n0 -> ?Goal0@{m:=m} (S n0)
+subgoal 3 is:
+ nat
+unification constraint:
+ 
+ n, m : nat |- ?Goal0@{m:=m} ?Goal2@{n:=n} <=
+   True /\ True /\ True \/
+   veeryyyyyyyyyyyyloooooooooooooonggidentifier =
+   veeryyyyyyyyyyyyloooooooooooooonggidentifier
diff --git a/test-suite/output/unifconstraints.v b/test-suite/output/unifconstraints.v
new file mode 100644
index 00000000..b9413a4a
--- /dev/null
+++ b/test-suite/output/unifconstraints.v
@@ -0,0 +1,22 @@
+(* Set Printing Existential Instances. *)
+Unset Solve Unification Constraints.
+Axiom veeryyyyyyyyyyyyloooooooooooooonggidentifier : nat.
+Goal True /\ True /\ True \/
+             veeryyyyyyyyyyyyloooooooooooooonggidentifier =
+             veeryyyyyyyyyyyyloooooooooooooonggidentifier.
+  refine (nat_rect _ _ _ _).
+  Show.
+Admitted.
+
+Set Printing Existential Instances.
+Goal forall n m : nat, True /\ True /\ True \/
+                        veeryyyyyyyyyyyyloooooooooooooonggidentifier =
+                        veeryyyyyyyyyyyyloooooooooooooonggidentifier.
+  intros.
+  refine (nat_rect _ _ _ _).
+  Show.
+  clear n. 
+  Show.
+  3:clear m.
+  Show.
+Admitted.