I don't think the Coq developers are inclined to chicken out, and the virility of a theorem prover shouldn't be underestimated. More concretely, there would be some confusion with the popular Chicken Scheme compiler.