3 files changed, 5 insertions, 5 deletions
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 09f032d478..f44465456f 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -48,8 +48,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 4116a5ebc2..a4d19d6930 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/inference.out b/test-suite/output/inference.out
index f2d1447785..c5a393408e 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 |- ?T0 -> T n]