aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/Case16.v
blob: ce9a0ecb4ad76ea4d0976ce354f182d76cf21f61 (plain)
1
2
3
4
5
6
7
8
9
10
(**********************************************************************)
(* Test dependencies in constructors                                  *)
(**********************************************************************)

Check
  (fun x : {b : bool | if b then True else False} =>
   match x return (let (b, _) := x in if b then True else False) with
   | exist _ true y => y
   | exist _ false z => z
   end).