github.com/coq/opam-coq-archive
A short constructive formalization of finitely presented modules
opam install coq-fpmods.0.2.0