summaryrefslogtreecommitdiff
path: root/test-suite/failure/Case5.v
blob: 70e5b98861307125b3f45b0c94b754eaeb8e915c (plain)
1
2
3
4
5
6
7
Inductive MS : Set :=
  | X : MS -> MS
  | Y : MS -> MS.

Fail Type (fun p : MS => match p return nat with
                    | X x => 0
                    end).