It seems that bedrock2 doesn't compile on the CI, likely due to an interaction with Ltac2.
Any idea what's going on?
see e.g. https://github.com/coq/coq/pull/14002/checks?check_run_id=2193554701
The error message is fishy, since AFAICT the Assert_failure exception is declared only once in that file.
Looks like a bug in the redeclaration check.
Reported here: https://github.com/coq/coq/issues/14003
I don't know why it wasn't caught by the CI.
Fix here: https://github.com/coq/coq/pull/14004
Last updated: Oct 13 2024 at 01:02 UTC