coq - 为什么 "only printing"符号会修改解析器

Question

manual说的是

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

所以我希望当我添加“仅打印”符号时，这些术语会被解析为没有符号。 但是，当我这样做时

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

术语1现在被解析为Bit

Check 1. (* 1 : Bit *)

为什么会发生这种情况以及如何添加 1 作为仅打印符号？

Answer 1

正如 Théo Winterhalter 提到的，这似乎是 Coq 8.13 中的一个错误。 根据this Github issue ，它似乎已在 Coq 8.14 8.15 中修复。