The Coq mailing list

[Marco Servetto <marco.servetto AT gmail.com>]

This library looks promising.
There is any documentation/guide/simple example of use of it?
(i'm not interested in exporting programs, i need it only to make proofs)

what is the meaning of
  Axiom eq_refl : forall m : t, eq m m.
  Axiom eq_sym : forall m1 m2 : t, eq m1 m2 -> eq m2 m1.
 ....
It looks like it assert that some function have some properties
instead of requiring the user to provide such proofs.
It is right?

And... err, my coq ignorance... what is the meaning of
"Parameter" it looks like it autodeclare a parameter with such
name/type in all the following function, but:
  -what is the scope of such declaration?
  -what is the difference with "Hypothesis"?