aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/failure/Case5.v
blob: 494443f1c988923c6506e3a5e1ebed069f2cff8a (plain)
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).