The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Marco Servetto wrote:
> Now, can I know what to do to instantiate my map and set?

From the OCaml manual, you should have learned the concept of 
"functor."  For instance, Coq module Coq.FSets.FSetAVL contains a 
functor for producing finite set implementations.  This should be a 
complete answer to the question of "how to instantiate a map or set"; I 
hope further questions can be more specific.

> Moreover, since setoid is required, Does setoid use extra axioms or not?

What makes you think "setoid is required"?

> Is there a standard way to know if a library I'm using does use extra
> axioms?
>    

See the vernacular command [Print Assumptions].