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: Oct 16 2021 at 03:02 UTC