The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

http://coq.inria.fr/refman/general-index.html says:

• Context, 4.2
• Context, 19.6.4

The latter (http://coq.inria.fr/refman/Reference-Manual022.html#hevea_default881) is the command.

-Jason

On Wed, Feb 19, 2014 at 6:35 AM, Frédéric Blanqui <frederic.blanqui AT inria.fr> wrote:

Great. Thank you!

The command "Context" does not appear in the index. :-(

Is it documented somewhere?

Le 19/02/2014 19:29, Jason Gross a écrit :

Context {var : type}.

Alternatively, use [Global Arguments lemma {var}.] after you close the section.

-Jason

On Wed, Feb 19, 2014 at 6:08 AM, Frédéric Blanqui <frederic.blanqui AT inria.fr> wrote:

Hello.

Is there a way to tell Coq that some section variable should be declared as a maximally inserted implicit argument when the section is closed?

Regards,

Frédéric.