1 files changed, 7 insertions, 0 deletions
diff --git a/test-suite/failure/Case12.v b/test-suite/failure/Case12.v
new file mode 100644
index 00000000..b56eac0d
--- /dev/null
+++ b/test-suite/failure/Case12.v
@@ -0,0 +1,7 @@
+
+Type [x:nat]<nat> Cases x  of 
+                  ((S x) as b) => <nat>Cases x  of
+                                        x => x 
+                                   end
+                          end.
+