2230.v « closed « bugs « test-suite - coq - the Coq proof assistant

about summary refs log tree commit diff homepage

path: root/test-suite/bugs/closed/2230.v

blob: 5076fb2bb7168f788cb8c41ddc7363137dbc6e07 (plain)

Goal forall f, f 1 1 -> True.
intros.
match goal with
  | [ H : _ ?a |- _ ] => idtac
end.
Abort.