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

summary refs log tree commit diff

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

blob: 0b8abace226596f80dd4504ec837d104dbbc8300 (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.