Integrate stdpp
The Coq library stdpp
https://gitlab.mpi-sws.org/iris/stdpp seems to be well maintained and provides a ready-to-use implementation of the map data structures, among other things. Connect this map data structure to our project in the environment file https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/docs/environment/map You can modify this environment file as you wish, and to know if the changes have a correct type you can re-compile the project.
I do not know if stdpp
provides the exact map implementation that we are looking for. For example, I have seen that they provide a https://plv.mpi-sws.org/coqdoc/stdpp/stdpp.gmap.html version that requires an encoding function in addition to a comparison function. If they do not provide other map implementations, it is always possible the existence of such encoding function. It will still be a net progress compared to what we have today.