Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

1 files changed, 9 insertions, 6 deletions

diff --git a/test-suite/failure/Case3.v b/test-suite/failure/Case3.v
index 2c651b87..ca450d5b 100644
--- a/test-suite/failure/Case3.v
+++ b/test-suite/failure/Case3.v
@@ -1,7 +1,10 @@
-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.
 
-Type [l:(List nat)]<nat>Cases l of 
-                         (Nil nat) =>O
-                      | (Cons  a l) => (S a)
-                      end.
+Type
+  (fun l : List nat =>
+   match l return nat with
+   | Nil nat => 0
+   | Cons a l => S a
+   end).