The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Marco Servetto wrote:
> Moreover It is also quite clear that there is some "standard well
> know" way to use abstract datastructures like this maps, but i have no
> idea what it is, is there a guide about it? some sort of documentation
> for "simple users".
> I came from Java, I know basic of ocaml, that is my knoledge stops in
> front of " locations for modifiable state" and "modules"
> in the sense that I know nothing about the two.
>    

Have you read Section 2.5 of the Coq manual, called "Module system"?  If 
that is not a sufficient introduction, have you read Chapter 2 of the 
OCaml manual, "The module system"?
    http://caml.inria.fr/pub/docs/manual-ocaml/manual004.html
OCaml's module system is the inspiration for Coq's.  Coq documentation 
is prone to avoid giving details on features that are inherited.