Add support for auto-generating Inductives for enums

Enums which are not annotated with a refined_by attribute get an auto-generated Coq Inductive they are refined by. Also start refactoring the whole Coq pretty printing business.