The Coq mailing list

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

We have a largeish Coq development (https://github.com/QuickChick/QuickChick) 
that is gaining users and deserves to be better documented.  

In the OCaml world, we’d do this by making a small number of .mli files 
containing just type declarations and signatures of all the externally useful 
functions.  Function bodies, auxiliary definitions, etc. are all hidden in 
.ml files that users of the library never look at.

On the other hand, in Coq, this seems not to be the default style, even for 
the standard library and thoughtfully packaged libraries like ExtLib; 
instead, library writers just sprinkle coqdoc comments near the main 
definitions in their .v files and nothing more — no separate interface files 
collecting just the user-facing bits.

Is there agreement in the community about how a library should best be 
structured so that its API is easy for users to grok, search, etc.?  Are 
there examples illustrating best practices?

Thanks!

    - Benjamin (and Leo and Zoe)