The Coq mailing list

[Ramana Kumar <ramana.kumar AT gmail.com>]

Of course, I agree.
For the meanwhile I have this list.
I'm also unsure about the intended use of MSets... do I have to pick
an implementation, or can I write to an abstract interface for finite
sets and fill in the implementation later (for code extraction
purposes, say) or never?
If I did want to do that, and if MSets is not suitable, then what
could I use instead?

I'm also still keen to hear of existing examples to look at. Cedric
Auger, thanks for yours. It seems like the only place you actually use
MSets there is with the call to MakeWithLeibniz, right?

On Thu, Nov 10, 2011 at 1:35 PM, Adam Chlipala 
<adamc AT csail.mit.edu>
 wrote:
> Incidentally, the commonness of this sort of question indicates a
> fundamental problem with coqdoc or even with Coq source file organization:
> there is no clear separation of implementation and interface.  Someone
> curious about how to use finite maps or sets should be able to look at a
> file, like .mli files in OCaml, that clearly specifies interfaces only.  As
> it stands now, to see, e.g., the best way to use the [FMapAVL] module, a
> newcomer has to know to scroll all the way to its bottom, past all manner of
> implementation details, to find the functor [Make]; and this description
> holds of the coqdoc output, too.
>