summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/shouldsucceed/1981.v
blob: 99952682d549064042a019c8a0ee7dc30a0f47ac (plain)
1
2
3
4
5
Implicit Arguments ex_intro [A].

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