1 files changed, 21 insertions, 0 deletions
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index a3033e94..9d0d0658 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -6,4 +6,25 @@ 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
+proj = 
+fun (x y : nat) (P : nat -> Type) (def : P x) (prf : P y) =>
+match eq_nat_dec x y with
+| left eqprf =>
+    match eqprf in (_ = z) return (P z) with
+    | refl_equal => def
+    end
+| right _ => prf
+end
+     : forall (x y : nat) (P : nat -> Type), P x -> P y -> P y
 
+Argument scopes are [nat_scope nat_scope _ _ _]
+foo = 
+fix foo (A : Type) (l : list A) {struct l} : option A :=
+  match l with
+  | nil => None (A:=A)
+  | x0 :: nil => Some x0
+  | x0 :: (_ :: _) as l0 => foo A l0
+  end
+     : forall A : Type, list A -> option A
+
+Argument scopes are [type_scope list_scope]