Ralf Jung (Feb 17 2021 at 14:39): Ralf Jung (Feb 17 2021 at 14:39):In Iris, we keep running into this longstanding ssreflect rewrite problem. Would anyone have an idea who could know the relevant code that is causing the bug?
Enrico Tassi (Feb 17 2021 at 14:54):Well, I pinged the right group of maintainer. Let's see if we @Gaëtan Gilbert or @Maxime Dénès can allocate some time. I'm probably the one that knows the buggy code better, I'm happy to help pointing them to the right piece of code, but I don't have much time myself to devote to this bugfix :-/
Ralf Jung (Feb 27 2021 at 09:30):@Gaëtan Gilbert came up with a fix :hearts: https://github.com/coq/coq/pull/13882
Guillaume Melquiond (Feb 27 2021 at 09:54):Note that it breaks quite a few developments. So, with my release manager hat on, I don't feel too thrilled about it right now.
Gaëtan Gilbert (Feb 27 2021 at 10:04):the iris failure looks strange, possibly a bug is involved
Last updated: Dec 07 2023 at 11:02 UTC