summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/2295.v
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).