2230.v « shouldsucceed « closed « bugs « test-suite - debian-coq - Debian packaging for Coq

summary refs log tree commit diff

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

blob: 5076fb2bb7168f788cb8c41ddc7363137dbc6e07 (plain)

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