aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/Case16.v
blob: 77016bbfe6e85ad0d2e0a631962cd7afe48c3715 (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).