QArithSternBrocot (coq-community project) broke hard in Coq 8.11. The reason was that Stdlib introduced a lemma
Zsgn_1, which took priority over the local
Zsgn_1 lemma (the lemmas had very similar parameters, but completely different statements). Seemingly, both Stdlib and QArithSternBrocot are full of lemma names like
Would it help to order stdlib imports before local imports? 8.11 changed the import semantics breaking everything...
Example fix in this style: https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/313
it probably would help, but the project is full of
Require Export ..., which makes figuring out order of imports a nightmare.
Last updated: Oct 16 2021 at 03:02 UTC