1981.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/1981.v

blob: 99952682d549064042a019c8a0ee7dc30a0f47ac (plain)

Implicit Arguments ex_intro [A].

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