blob: 50221cdd83a540af6093e56b9f96520eea0155ae (
plain)
1
2
3
4
5
6
7
8
9
10
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.
|
