coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Context declaration

From: St�phane Lescuyer <stephane.lescuyer AT inria.fr>
To: Arthur Azevedo de Amorim <arthur.aa AT gmail.com>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Context declaration
Date: Mon, 11 May 2009 18:22:19 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:date :x-google-sender-auth:message-id:subject:from:to:cc:content-type :content-transfer-encoding; b=qtZ//Hvk8pvSk/0yh4WaicoeCluoDfO95HAc4/uDgJEg66SUx1ZOA9e21hByy6kgE2 W4kztdxjwFcyshNfwH1c8Fs3ZIO9Z99m07PtPrfORjirKae3aX4HZobmoh+00LPpCjh+ Uf1YbCtYERfV6ds9DQba8GAusIdCb1H6e/nE0=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

I was just about to send an email to Matthieu to ask for such a
command (I was very annoyed recently with the apparent impossibility
to define instance variables in sections), now it turns out that it is
already implemented but just lacks documentation :-) Thank you very
much Arthur for spotting that, I read that paper months ago and I had
forgotten about that.

St�phane L.

On Mon, May 11, 2009 at 5:57 PM, Arthur Azevedo de Amorim
<arthur.aa AT gmail.com>
wrote:
> 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
>

--
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06

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