The Coq mailing list

[Michael Shulman <mshulman AT ucsd.edu>]

Thank you!  I am sorry to be a bother; for some inexplicable reason I
was reading the 8.2 reference manual instead of the 8.3 one.

On Mon, Nov 21, 2011 at 16:03, Tom Prince 
<tom.prince AT ualberta.net>
 wrote:
> 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
>
>