diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-13 17:21:24 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-13 19:12:34 +0200 |
| commit | 954ae934849d6af88e8b20e6b69cffbb341a3cf9 (patch) | |
| tree | 5d1f061e8f9d3af7b0b83521be715449dbdcf7fd /test-suite/success | |
| parent | d24e6d915d0170d5d3e9690c053a0b0b4c2758e5 (diff) | |
Added support for several impossible cases in compilation of "match".
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/Case21.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/test-suite/success/Case21.v b/test-suite/success/Case21.v index 3f7877456..db91eb402 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. |