RecordsNotModules
The main bulk of the modules and functor system can be replaced by dependent record types and functions instead. Because of this, there is little reason to use modules other than to provide namespace support. In fact, there are good reasons not to use modules. Most importantly, module parameters cannot be instantiated with variables. See Carlos Simpson's post to coq-club.
See Coq's standard library for examples of how to do this.
Note that the TypeClasses feature uses dependent records internally to provide modularity.
To the extent possible under law, the contributors of the Rocq wiki have waived all copyright and related or neighboring rights to their contributions.
By contributing to the Rocq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.