blob: 584edf19b9a540cba8235c542f92359061f89a5b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
(* Check if omission of "as" in return clause works w/ section variables too *)
Section sec.
Variable b: bool.
Definition d' :=
(match b return b = true \/ b = false with
| true => or_introl _ (refl_equal true)
| false => or_intror _ (refl_equal false)
end).
End sec.
|
