coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Reserved Notation bug?

From: Tom Prince <tom.prince AT ualberta.net>
To: AUGER Cédric <sedrikov AT gmail.com>, Jason Gross <jasongross9 AT gmail.com>
Cc: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Reserved Notation bug?
Date: Sun, 07 Oct 2012 14:48:39 -0600

AUGER Cédric
<sedrikov AT gmail.com>
writes:
> I guess it is a bug. Replacing curly braces makes it work:

{} has special status, see the third remark here:
http://coq.inria.fr/doc/Reference-Manual015.html#htoc374

Re: [Coq-Club] Reserved Notation bug?, Tom Prince, 10/07/2012