1 files changed, 18 insertions, 20 deletions
diff --git a/test-suite/failure/Case7.v b/test-suite/failure/Case7.v
index 3718f198..64453481 100644
--- a/test-suite/failure/Case7.v
+++ b/test-suite/failure/Case7.v
@@ -1,22 +1,20 @@
-Inductive listn : nat-> Set := 
-  niln : (listn O) 
-| consn : (n:nat)nat->(listn n) -> (listn (S n)).
+Inductive listn : nat -> Set :=
+  | niln : listn 0
+  | consn : forall n : nat, nat -> listn n -> listn (S n).
 
-Definition length1:= [n:nat] [l:(listn n)]
-                    Cases l of 
-                     (consn n _ (consn m _ _)) => (S (S m))
-                    |(consn n _ _) => (S O)
-                    | _ => O
-                    end.
-
-Type [n:nat]
-       [l:(listn n)]
-        <nat>Cases n of 
-            O  => O
-        |  (S n)  =>
-             <([_:nat]nat)>Cases l of 
-                 niln  => (S O)
-              |  l'  => (length1 (S n) l')
-             end
-       end.
+Definition length1 (n : nat) (l : listn n) :=
+  match l with
+  | consn n _ (consn m _ _) => S (S m)
+  | consn n _ _ => 1
+  | _ => 0
+  end.
 
+Type
+  (fun (n : nat) (l : listn n) =>
+   match n return nat with
+   | O => 0
+   | S n => match l return nat with
+            | niln => 1
+            | l' => length1 (S n) l'
+            end
+   end).