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 pattern
/ destruct
matching treat monomorphic-polymorphic comparisons differently from homogenous comparisons. See https://github.com/coq/coq/issues/17168 for more details.
Last updated: Oct 13 2024 at 01:02 UTC