aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/if.v
blob: c81d2b9bf1b8973c43750198effe774c65becc67 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
(* The synthesis of the elimination predicate may fail if algebric *)
(* universes are not cautiously treated *)

Check (fun b : bool => if b then Type else nat).

(* Check correct use of if-then-else predicate annotation (cf BZ#690) *)

Check fun b : bool =>
 if b as b0 return (if b0 then b0 = true else b0 = false)
 then refl_equal true
 else refl_equal false.