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