summaryrefslogtreecommitdiff
path: root/test-suite/failure/Case12.v
blob: 4a77f139cb3ed7ee1c6d197af8e859160d5a7d78 (plain)
1
2
3
4
5
6
7
8

Fail Type
  (fun x : nat =>
   match x return nat with
   | S x as b => match x with
                 | x => x
                 end
   end).