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

summary refs log tree commit diff

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

blob: a3d94293070ee09e6aded04f500b2cf00bcf6ff3 (plain)

Arguments ex_intro [A].

Goal exists n : nat, True.
  eapply ex_intro. exact 0. exact I.
Qed.