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

summary refs log tree commit diff

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

blob: 4b187224311e9c57c7d20bd47cc596f7dca1279d (plain)

Goal forall A B, A * B -> A.
Proof.
intros A B H.
match goal with
  | [ H : _ * _ |- _ ] => exact (fst H)
end.
Qed.