blob: 68d26ac8df77934b1ea3b46aeb0ac9b5776f4076 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
(* The synthesis of the elimination predicate may fail if algebraic *)
(* 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.
|
