coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] implicit arguments / sections

From: Vladimir Voevodsky <vladimir AT ias.edu>
To: Coq-Club Club <coq-club AT inria.fr>
Subject: [Coq-Club] implicit arguments / sections
Date: Wed, 29 Jun 2011 10:27:53 -0400

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 ?

Thanks!
Vladimir.

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