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

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