summaryrefslogtreecommitdiff
path: root/test-suite/failure/Case13.v
blob: 5c0aa3e12d44b91670cff3d515cb0b8199d7e36e (plain)
1
2
3
4
5
6
7
Fail Type
  (fun x : nat =>
   match x return nat with
   | S x as b => match x with
                 | x => S b x
                 end
   end).