Module System

• Introduction to modules through a ModuleSystemTutorial.
• ModulesForTheories: Using modules and records to capture mathematical theories.
• RecordsNotModules: Why you shouldn't use the module system at all, and use dependent records instead.
• ModulesNotRecords: Why the previous line does not always stand.
• ProofTermsConsideredHarmful: Why using dependent records can be difficult, and sometimes inadvisable.
• ModulesBibliography: Various pointers to modules in systems like Coq.
• OpenIssuesWithModules: A discussion on various issues about Coq module system and how to address them.