blob: b7f06dcf632f95a2d2d565a702ba94fb961613ad (
plain)
1
2
3
4
5
6
7
|
(* Check correct use of if-then-else predicate annotation (cf bug 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.
|