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

Check [x : {b:bool|if b then True else False}]
   <[x]let (b,_) = x in if b then True else False>Cases x of
   | (exist true y)  => y
   | (exist false z) => z
   end.