I just got a CI failure in std++ when building against Coq master: https://gitlab.mpi-sws.org/iris/stdpp/-/jobs/101569
Shouldn't Coq CI have prevented this?
hm, also then it should have already failed last night...
ah the regression only arises with name mangling enabled
Last updated: Feb 06 2023 at 00:03 UTC