What about `Universe Minimization ToSet`?
Follow-up from https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/merge_requests/34/diffs#note_28380 :
The problem only really comes up when you build more layers of definitions on top of this. At some point, Coq will decide that you don't really need all those universes and
Set
is good enough for some of them. (But it's never good enough..)Although maybe this might really not be a problem here since this would be an issue in other universe polymorphic files, not this one. In any case, if you ever wanted to add more definitions to this file, you might still benefit from unsetting minimization.
In that base, it may make more sense to add it globally to
base.v
?
Maybe we should investigate why this option is not enabled by default.
Probably performance? Minimizing to
Set
reduces the universe graph.
@amintimany Could you give us some advice here?