In `gmap.v`, we don't properly escape [this line](https://gitlab.mpi-sws.org/iris/stdpp/-/blob/375341e746af2d30fb8a65b80766db027eefbbb6/stdpp/gmap.v#L20). As such, [the coqdoc](https://plv.mpi-sws.org/coqdoc/stdpp/stdpp.gmap.html) omits the rest of the comment block. This should be a quick fix, but I don't have fork permissions to make a MR.