1 files changed, 13 insertions, 0 deletions
diff --git a/test-suite/failure/Case2.v b/test-suite/failure/Case2.v
new file mode 100644
index 00000000..183f612b
--- /dev/null
+++ b/test-suite/failure/Case2.v
@@ -0,0 +1,13 @@
+Inductive IFExpr : Set := 
+          Var  : nat -> IFExpr
+        | Tr   : IFExpr
+        | Fa   : IFExpr
+        | IfE   : IFExpr -> IFExpr -> IFExpr -> IFExpr.
+
+Type [F:IFExpr]
+    <Prop>Cases F of
+       (IfE (Var _) H I) => True
+     | (IfE _ _ _)   => False
+     |  _          => True
+     end.
+