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: 0c3b96dad924a3653f1521776261b660c929043e (plain)

Implicit Arguments ex_intro [A].

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