blob: f5ca28dcaa8a368583ef86893b1430e0a14f0749 (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
(* 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).
|
