summaryrefslogtreecommitdiff
path: root/test-suite/failure/Case8.v
blob: 035629fef5e6e5d0d149e931c41b6efefd467929 (plain)
1
2
3
4
5
6
7
8
Inductive List (A : Set) : Set :=
  | Nil : List A
  | Cons : A -> List A -> List A.

Fail Type match Nil nat return nat with
     | b => b
     | Cons _ _ _ as d => d
     end.