diff options
Diffstat (limited to 'test-suite/bugs/closed/5460.v')
| -rw-r--r-- | test-suite/bugs/closed/5460.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/5460.v b/test-suite/bugs/closed/5460.v new file mode 100644 index 00000000..50221cdd --- /dev/null +++ b/test-suite/bugs/closed/5460.v @@ -0,0 +1,11 @@ +(* Bugs in computing dependencies in pattern-matching compilation *) + +Inductive A := a1 | a2. +Inductive B := b. +Inductive C : A -> Type := c : C a1 | d : C a2. +Definition P (x : A) (y : C x) (z : B) : nat := + match z, x, y with + | b, a1, c => 0 + | b, a2, d => 0 + | _, _, _ => 1 + end. |