coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] implicit arguments / sections

From: Mehdi Dogguy <mehdi AT dogguy.org>
To: Vladimir Voevodsky <vladimir AT ias.edu>
Cc: Coq-Club Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] implicit arguments / sections
Date: Wed, 29 Jun 2011 16:37:36 +0200

On 29/06/2011 16:27, Vladimir Voevodsky wrote:
> Hello,
>
> is there a way to make some of the arguments which appear after the
> closure of a section in the definitions etc. built inside a section to
> be implicit ?
>

I guess you need Context statements.

http://coq.inria.fr/refman/Reference-Manual024.html#@default865

Regards,

--
Mehdi Dogguy مهدي الدڤي
http://dogguy.org/

[Coq-Club] implicit arguments / sections, Vladimir Voevodsky
- Re: [Coq-Club] implicit arguments / sections, Mehdi Dogguy