summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/4656.v
blob: c89a86d634880cd7fada31fffe20186648b3b6e9 (plain)
1
2
3
4
(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *)
Goal True.
  constructor 1.
Qed.