7 files changed, 25 insertions, 9 deletions
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 09f032d47..2b828d382 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,8 +50,8 @@ 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
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 4116a5ebc..a4d19d693 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -72,8 +72,8 @@ 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.
diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out
index bbfd3405a..c17c63e72 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/PrintInfos.out b/test-suite/output/PrintInfos.out
index ba076f050..98420409e 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
diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out
index 4512e2c5c..576fbd7c0 100644
--- a/test-suite/output/inference.out
+++ b/test-suite/output/inference.out
@@ -6,7 +6,7 @@ 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 |- ?T -> T n] 
diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out
index d003c70df..20e274e25 100644
--- a/test-suite/output/ltac.out
+++ b/test-suite/output/ltac.out
@@ -1,2 +1,5 @@
 The command has indeed failed with message:
 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
diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v
index 7e2610c7d..373b870b9 100644
--- a/test-suite/output/ltac.v
+++ b/test-suite/output/ltac.v
@@ -15,3 +15,13 @@ 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.