The Coq mailing list

["Benjamin C. Pierce" <bcpierce AT cis.upenn.edu>]

I would love to see (an expanded version of) this discussion written down 
carefully somewhere!!

  - B

> On Aug 20, 2018, at 3:17 AM, Soegtrop, Michael 
> <michael.soegtrop AT intel.com>
>  wrote:
> 
> 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
>