lastland
commented
3 years ago 
Sounds like a good plan. I'd recommend polymorphic Mod.val and either cumulative Mod.val or polymorphic cumulative Mod.val to be consistent with the current set of edits. We'll probably need to add a new map from names to their polymorphism status, and then monitor that flag that when translating. (Are polymorphism and cumulativity independent? That probably affects the design.) This should be decently straightforward to add, although it will necessitate modifying the Coq AST to include the Polymorphic and Cumulative tags. I need to focus on my dissertation instead of implementing this, though.
It seems that an edit that makes a definition polymorphic would be helpful. I know that Eric has already been working on this, and I am opening this issue to list a few use cases I found.
The most basic form would be something like
set Foo.bar polymorphicwhereFoo.baris the qualified name of a definition. The definition can be a record, a type class, a type class instance, a function, an inductive or a coinductive data type, a variant, or a lemma/theorem/axiom (I have found scenarios where I want to make a lemma polymorphic)...Ideally, when the definition is an instance, we will also want to make all its class methods polymorphic (in Coq translations, they are separate definitions).
When the definition is an inductive or coinductive data type, a variant, or a record type, it would also be useful if a single edit can make it polymorphic and cumulative (maybe something like
set Foo.bar polymorphic cumulative?)---the definition would not be cumulative by default otherwise (see: https://coq.inria.fr/refman/addendum/universe-polymorphism.html#cumulative-noncumulative).In some scenarios, we may also want to use a single edit to make everything in a module universe polymorphic. And in those scenarios, we may also want edits that can make a few definitions monomorphic.