1 files changed, 12 insertions, 11 deletions
diff --git a/test-suite/success/Case7.v b/test-suite/success/Case7.v
index 6e2aea48..6e4b2003 100644
--- a/test-suite/success/Case7.v
+++ b/test-suite/success/Case7.v
@@ -1,16 +1,17 @@
-Inductive List [A:Set] :Set := 
- Nil:(List A) | Cons:A->(List A)->(List A).
+Inductive List (A : Set) : Set :=
+  | Nil : List A
+  | Cons : A -> List A -> List A.
 
-Inductive Empty [A:Set] : (List A)-> Prop := 
-  intro_Empty: (Empty A (Nil A)).
+Inductive Empty (A : Set) : List A -> Prop :=
+    intro_Empty : Empty A (Nil A).
 
-Parameter inv_Empty : (A:Set)(a:A)(x:(List A)) ~(Empty A (Cons A a x)).
+Parameter
+  inv_Empty : forall (A : Set) (a : A) (x : List A), ~ Empty A (Cons A a x).
 
 
 Type
-[A:Set] 
-[l:(List A)]
-  <[l:(List A)](Empty A l) \/ ~(Empty A l)>Cases l of 
-        Nil  =>  (or_introl ? ~(Empty A (Nil A)) (intro_Empty A))
-   |  ((Cons a y) as b) =>  (or_intror (Empty A b) ? (inv_Empty A a y))
-  end.
+  (fun (A : Set) (l : List A) =>
+   match l return (Empty A l \/ ~ Empty A l) with
+   | Nil => or_introl (~ Empty A (Nil A)) (intro_Empty A)
+   | Cons a y as b => or_intror (Empty A b) (inv_Empty A a y)
+   end).