The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Oh, and I forgot to recall it,

The advantage of Modules over Records are just:
→ name space management
→ notations management
→ tactics management
→ Extraction (to Ocaml)
→ interactive definitions
→ inclusion of other modules via Inline/Include
→ subtyping

For all other stuff, I prefer using Records, as I find them a lot more
convenient (and they do not require additionnal knowledge on Coq
mechanics once you know of how Inductive works).

And I hardly ever need any of the above mentionned stuff.

→ Name space management can be done through files (yes, I know they are
  Modules, but they are special modules, as AFAIK, you cannot implement
  a Functor [In Ocaml sense] through files)
→ Notations inside of a Module (not being a file) are not that common
→ Same for tactics
→ Well, for extraction I agree that using a Record would lead to
  an Obj.t inside of it if some type field is involved.
  Maybe could such Records be extracted to first class modules (I am
  not a big user of first class modules, so I cannot tell if it is
  relevant)
→ interactive definitions can partly be done via the "refine" tactic
→ inclusion cannot be done with records, but honestly, I never use this
  feature, and I really hate to have to jump from one module to an
  other in the documentation to understand what a module using imports
  contains (and I think I am not the only one, seeing how many post
  have occured on asking how does OrderedType work to build a
  FMap/FSet).
→ I never used subtyping with Modules. I know that the Coercion command
  is not as handy as automatic management of it through modules.
  Once again, it is not that often that subtyping is useful, and there
  are still cases where you cannot do it conveniently even with modules.

So if you really need Modules (for instance because you have to use the
standard library for Sets/Maps, or need to extract to Ocaml), I am sorry
for you. Else I think it is worth to change your project to have to
deal with Records rather than with Modules.