aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/bug_3146.v
blob: c42e28818a6a2f4a834bfb94df8d1627f8e7254d (plain)
1
2
3
4
5
Axiom x : True.
Goal nat -> nat.
  intro x.
  abstract (exact x).
Qed.