coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Gyesik Lee <gslee AT ropas.snu.ac.kr>
- To: Coq Club <coq-club AT inria.fr>
- Subject: [Coq-Club] Deactivation of the printing "some" notations
- Date: Tue, 16 Nov 2010 12:14:59 +0900
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:from:date:x-google-sender-auth:message-id :subject:to:content-type; b=gQBrOVv8zgUuSRvI+InssXp98nV+qoQOsdpi0p9hiJNj9kCd1jn5CTwKIjyXr+CQ8t MYrpzZAmgwTuDimL39MQ9QLzqS4hafROEAP+klzv00nwn4Y2DocAy1f2wEVeSXCs0gR5 LScaAOa5DXM4o/HwMVlx3CxIsI7+u23voPefQ=
Hi,
I am wondering if there is a way to deactivate/activate printing "only
some" notations.
In the reference, there is only a way to deactivate/activate printing
"all" notations.
Gyesik
- [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
- [Coq-Club] Ltac: first [] and ||,
AUGER Cedric
- Re: [Coq-Club] Deactivation of the printing "some" notations,
Martijn Vermaat
Archive powered by MhonArc 2.6.16.