Stream: Coq devs & plugin devs

Topic: Universe Polymorphism incompatibilities


view this post on Zulip Jason Gross (Jan 25 2023 at 17:25):

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: Jun 13 2024 at 03:02 UTC