From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 28 Apr 2006 14:59:16 +0000
Subject: Imported Upstream version 8.0pl3+8.1alpha

---
 test-suite/failure/Case5.v | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'test-suite/failure/Case5.v')

diff --git a/test-suite/failure/Case5.v b/test-suite/failure/Case5.v
index bdb5544b..29996fd4 100644
--- a/test-suite/failure/Case5.v
+++ b/test-suite/failure/Case5.v
@@ -1,3 +1,7 @@
-Inductive MS: Set := X:MS->MS | Y:MS->MS.
+Inductive MS : Set :=
+  | X : MS -> MS
+  | Y : MS -> MS.
  
-Type  [p:MS]<nat>Cases p of (X x) => O end.
+Type (fun p : MS => match p return nat with
+                    | X x => 0
+                    end).
-- 
cgit v1.2.3