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.
refined_by
