I've managed to track down one of the incompatibilities that commonly pops up when trying to make developments universe polymorphic, and is probably at least partially responsible for the fact that if you
Set Universe Polymorphism in some places but not others, this breaks code that would work both if you set it everywhere and also if you set it nowhere: it seems that
destruct matching treat monomorphic-polymorphic comparisons differently from homogenous comparisons. See https://github.com/coq/coq/issues/17168 for more details.
Last updated: Nov 29 2023 at 04:01 UTC