The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi all,

Is there any way in Coq to have a "printing-only" notation?  There is
"only parsing", but "only printing" does not seem possible right now.
Such a flag would be nice to have for notations that, if made "parsing",
trigger some horrible conflicts.  If these constructions mostly appear
as intermediate state, even if the notation cannot be written, it makes
the current goal much more readable.  Another use case is an "embedded
proof mode", where we want to render our own "named context" (because
there is some structure there which makes it impossible to use Coq's
context).  We never want to write these contexts, but when displayed,
they should be rendered as closely as possible to Coq's context.

Right now, we use some horrible hacks Robbert came up with that involve
"zero-width whitespaces" as keywords for the notation, so that Coq
accepts it and does not create conflicts all over the place. This is
very confusing when editing the file that defines the notation, and even
worse, some editors (like emacs) actually display such "zero-width"
character as just having "almost zero width", so the alignment of
characters is just a few pixels off.

Having "printing only" notation would very useful.

Kind regards,
Ralf