(* -*- coq-prog-args: ("bugs/closed/PLACEHOLDER.v") -*- *)