coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Re: Notation which uses parameters of a Record/Class?

From: Bas Spitters <spitters AT cs.ru.nl>
To: Adam Megacz <megacz AT cs.berkeley.edu>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Re: Notation which uses parameters of a Record/Class?
Date: Thu, 15 Apr 2010 09:03:26 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:from:date :x-google-sender-auth:message-id:subject:to:cc:content-type :content-transfer-encoding; b=tzFP8FxcUfhd0AR+B4daNXLArUWUWiWYyiyf8S+PRS35FPUJDrOmJ/CgO0M+FIJmtq vBdP8x7jbo4XumcKWp36ehqsc/n/0SdKlXQAPxYVFP891+MJHBKbal/i+euEfh+dnuEu gXD8bTuTaDAS6nwHBTH3CUECxyC/KI45W74TU=

On Thu, Apr 15, 2010 at 5:45 AM, Adam Megacz
<megacz AT cs.berkeley.edu>
wrote:
> By the way, how is the [Context] command different from [Variable]? �I
> can't find [Context] in the manual:
>
> �http://www.lix.polytechnique.fr/coq/refman/command-index.html
>
> but my version of Coq certainly accepts it, and I see it appears once in
> the Sozeau+Oury paper. �Is it just another synonym for [Variable]?

From the trunk version of the documentation:

18.6.4 Context binder1 �bindern

Declares variables according to the given binding context, which might
use implicit generalization (see 18.4).

Bas

[Coq-Club] Notation which uses parameters of a Record/Class?, Adam Megacz
- Re: [Coq-Club] Notation which uses parameters of a Record/Class?, Bas Spitters
- Re: [Coq-Club] Notation which uses parameters of a Record/Class?, AUGER C�dric
- Message not available
  - [Coq-Club] Re: Notation which uses parameters of a Record/Class?, Adam Megacz
    - Re: [Coq-Club] Re: Notation which uses parameters of a Record/Class?, Bas Spitters
    - Re: [Coq-Club] Re: Notation which uses parameters of a Record/Class?, AUGER C�dric
    - Message not available
      - [Coq-Club] modules in sections (was: Notation which uses parameters of a Record/Class?), Adam Megacz