coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Deactivation of the printing "some" notations

From: Martijn Vermaat <martijn AT vermaat.name>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Deactivation of the printing "some" notations
Date: Tue, 16 Nov 2010 10:46:36 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=vermaat.name; h=subject:from :reply-to:to:in-reply-to:references:content-type:date:message-id :mime-version:content-transfer-encoding; q=dns; s=vermaat.name; b=Tb9oiagD0lAYSyePAbjs0aGDCDSFRb8FR9zSDmwxVI+yyKpJbmhP+sb8bgrAD jBRwuGwIPIFjMuFg84N/blFFCe3dSaTfMraiPTybTPdH2Pfyo0lXwikFNy++WkES P6BbZzqFpDEn6fTtuI1SoA9TVEAN/u2ogKaixnhXdDnJk4=

> I am wondering if there is a way to deactivate/activate printing "only
> some" notations.

Are you familiar with the 'only parsing' modifier for the Notation
command?

http://coq.inria.fr/refman/Reference-Manual015.html#@command244

Depending of what you want exactly, this may not be enough for you,
since it can only be used directly with the declaration of a notation.

[Coq-Club] Deactivation of the printing "some" notations, Gyesik Lee
- Re: [Coq-Club] Deactivation of the printing "some" notations, Martijn Vermaat
  - [Coq-Club] Ltac: first [] and ||, AUGER Cedric
    - Re: [Coq-Club] Ltac: first [] and ||, St�phane Lescuyer