bug_2828.v « closed « bugs « test-suite - coq - The formal proof system

about summary refs log tree commit diff

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

blob: 36ac4605f455849e4944bc9e6f477db2ed3bdcf0 (plain)

Parameter A B : Type.
Coercion POL (p : prod A B) := fst p.
Goal forall x : prod A B, A.
  intro x. Fail exact x.
Abort.