coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Context declaration

From: Arthur Azevedo de Amorim <arthur.aa AT gmail.com>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] Context declaration
Date: Mon, 11 May 2009 16:57:45 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:content-type; b=akc7zcGuX73WLZUiu1vWfyDjUGwvjjEI1PA/f0bmQH8T6KCND6o78ue24U8IIezE8L 98oewdL2V+Jd/ifWWOlvp/HRU/gqnAsPVAFTU3O/YFXzesXrK/R98n06DNgjzQhXtZ22 yfNrVY+iMZQo6cX3Q0Wq8P4AkCKJtKs9zRbeY=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

At a first glance, it seemed to me that the "Context" command that appears on the paper on type classes is not documented. It would be nice to have it on the Coq manual!

--
Arthur Azevedo de Amorim

[Coq-Club] Context declaration, Arthur Azevedo de Amorim
- Re: [Coq-Club] Context declaration, St�phane Lescuyer
  - Re: [Coq-Club] Context declaration, St�phane Lescuyer