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?