The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Kevin,

I agree that some decisions in the standard library on what are modules and 
what are module types, what are functors and what not and how component 
modules/module types are combined to larger entities are suboptimal. Actually 
I repackaged many of the standard library modules, e.g. on orders, in a 
different way. Afaik Maxime started to work on a new version of the library - 
we should make this a good example on how modules should be used and add some 
explanations on the rationale. In my experience if one keeps the "module 
interfaces belong in module types" idea in mind, things work out quite 
naturally and unproblematic.

As I said, if you have specific issues, I would like to look over them and 
see if I can fix them or also review your usage of modules. Maybe I write 
some pages on the topic from a users / software engineering perspective and 
for this it would help to understand what issues other people have.

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928