aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/failure/Case14.v
blob: 29cae76456a4cd641aaea2aa812baddcbce148f5 (plain)
1
2
3
4
5
6
7
8
9
Inductive List (A : Set) : Set :=
  | Nil : List A
  | Cons : A -> List A -> List A.

Definition NIL := Nil nat.
Fail Type match Nil nat return (List nat) with
     | NIL => NIL
     | _ => NIL
     end.