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?
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 :-/
@Gaëtan Gilbert came up with a fix :hearts: https://github.com/coq/coq/pull/13882
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.
the iris failure looks strange, possibly a bug is involved
Last updated: Jun 09 2023 at 08:01 UTC