Imported Upstream version 8.0pl1upstream/8.0pl1

1 files changed, 22 insertions, 0 deletions

diff --git a/test-suite/failure/Case7.v b/test-suite/failure/Case7.v
new file mode 100644
index 00000000..3718f198
--- /dev/null
+++ b/test-suite/failure/Case7.v
@@ -0,0 +1,22 @@
+Inductive listn : nat-> Set := 
+  niln : (listn O) 
+| consn : (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.
+