1 files changed, 21 insertions, 3 deletions
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 09f032d47..8ce6f9795 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".