aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/2230.v
blob: 5076fb2bb7168f788cb8c41ddc7363137dbc6e07 (plain)
1
2
3
4
5
6
Goal forall f, f 1 1 -> True.
intros.
match goal with
  | [ H : _ ?a |- _ ] => idtac
end.
Abort.