`util/seqset.v` fails to build on coq:dev (the upcoming Coq 8.10)
Prosa is currently broken on the development version of Coq and requires a fix like this one: https://github.com/math-comp/finmap/commit/4cf617b5b0af8ed2b48360feb8a1e28a323cdbfe.
I have a patch ready in https://gitlab.mpi-sws.org/bbb/prosa/commits/fix-build-failure-in-coq-dev, but it breaks compatibility with mathcomp 1.8.0 on Coq 8.9, which I believe is still used by some.
In the long run, it would be good if we could retire our own homegrown version of finite sets in favor of the forthcoming finmap library in mathcomp.