(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *)
Goal True.
  constructor 1.
Qed.