The Coq mailing list

[Tom Prince <tom.prince AT ualberta.net>]

On Mon, 21 Nov 2011 14:27:56 -0800, Michael Shulman 
<mshulman AT ucsd.edu>
 wrote:
> Thank you!  Where can I find documentation about "Context"?  It is not
> in the index of the Coq reference manual.  Nor is your "Generalizable
> Variable" -- what does that do?

Context:
http://coq.inria.fr/refman/Reference-Manual024.html#toc135
This is exactly like Hypothesis, etc, except that it uses binder
notation, allowing {} for implicit arguments.

Generalizable Variable: (under section 2.7.17)
http://coq.inria.fr/refman/Reference-Manual004.html#toc20
This allows you to write something like `{x = y} for
forall x y, x = y
and also affects binders as described in 
http://coq.inria.fr/refman/Reference-Manual024.html#toc133
basically, only the name is optional, but the type is required, and the
implicitness of arguments is handled differently.

  Tom