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