coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Silencing "Warning: This notation will not be used for printing as it is bound to a single variable" in records

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Silencing "Warning: This notation will not be used for printing as it is bound to a single variable" in records
Date: Tue, 31 Jul 2012 04:18:35 -0400

Hi,

Is it possible to silence "Warning: This notation will not be used for printing as it is bound to a single variable" on something like

Reserved Notation "'foo'".

Record bar := { baz : Type where "'foo'" := baz }.

? I know in general I can use [(only parsing)], but [Reserved Notation] doesn't use it, and [where] clauses don't accept it, syntactically, in so far as I can tell.

Thanks.

-Jason

[Coq-Club] Silencing "Warning: This notation will not be used for printing as it is bound to a single variable" in records, Jason Gross, 07/31/2012