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.

added frontend label

enabled an automatic merge when the pipeline for c3b0bafc succeeds

mentioned in commit 85f1342c

merged