The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Marco Servetto wrote:
> > What makes you think "setoid is required"?
> >      
> -Library Coq.FSets.FMapInterface
> requires
> -Library Coq.Structures.DecidableType
> that requires
> -Library Coq.Lists.SetoidList
> -that requires
> Library Coq.Setoids.Setoid
>    

I'm pretty sure you can ignore this fact.  [Print Assumptions] will help 
you be sure in the end.

> It tooks me a long time to realize that the module/functor
> implementing the interface was the one called Raw.... It makes sense
> with the idea of hiding the implementation, however it isn't making it
> a little to extreem? may be someone want to depend of the
> implementation...
>    

I don't think you want to use that functor.  Just call, e.g., 
[FSetAVL.Make].  Its manual page has a hyperlink from the signature, 
where you can find all the members of the output module documented.  I 
think it's really that simple.