From 954ae934849d6af88e8b20e6b69cffbb341a3cf9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 13 Oct 2014 17:21:24 +0200
Subject: Added support for several impossible cases in compilation of "match".

---
 test-suite/success/Case21.v | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/Case21.v b/test-suite/success/Case21.v
index 3f78774565..db91eb402e 100644
--- a/test-suite/success/Case21.v
+++ b/test-suite/success/Case21.v
@@ -9,3 +9,7 @@ Inductive I : bool -> bool -> Prop := C : I true true.
 Check fun x (H:I x false) => match H with end : False.
 
 Check fun x (H:I false x) => match H with end : False.
+
+Inductive I' : bool -> Type := C1  : I' true | C2 : I' true.
+
+Check fun x : I' false => match x with end : False.
-- 
cgit v1.2.3