为什么"only printing"表示法会修改解析器

Question

手册上说

如果给定的符号字符串只出现在打印规则中，则解析器根本不会被修改。

所以我希望当我添加"only printing"符号，这些项就像没有符号一样被解析。但是，当我这样做时

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

术语1现在被解析为Bit

Check 1. (* 1 : Bit *)

为什么这种情况发生在这里，我如何添加1仅作为打印符号?

Answer 1

正如thWinterhalter所提到的，这似乎是Coq 8.13中的一个bug。根据这个Github问题，Coq8.148.15似乎已经修复。