Search code examples
coqnotation

Why does an "only printing" notation modify the parser

The manual says that

If a given notation string occurs only in only printing rules, the parser is not modified at all.

So I would expect that when I add an "only printing" notation, the terms are parsed as if there was no notation. However, when I do this

Inductive Bit := One | Zero.
Notation "1" := One (only printing).

The term 1 is now parsed as a Bit

Check 1. (* 1 : Bit *)

Why does this happen here and how can I add 1 as only a printing notation?

Solution

  • As Théo Winterhalter mentioned, this seems to be a bug in Coq 8.13. According to this Github issue, it seems to be fixed in Coq 8.14 8.15.