test-suite/failure/Case5.v


1
2
3
4
5
6
7

Inductive MS : Set :=
  | X : MS -> MS
  | Y : MS -> MS.

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