Karl Palmskog (Oct 09 2020 at 21:29): Karl Palmskog (Oct 09 2020 at 21:29):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 Z<blah>_<number>...
Paolo Giarrusso (Oct 10 2020 at 05:42):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
Karl Palmskog (Oct 10 2020 at 11:03):it probably would help, but the project is full of Require Export ..., which makes figuring out order of imports a nightmare.
Last updated: Apr 20 2024 at 14:01 UTC