Coq定义多构造子归纳命题报错：引用未在当前环境找到

问题现象 #

定义包含多个构造子的归纳命题时频繁出现未找到引用的错误，但仅保留单个构造子时可正常运行：

• 多构造子示例1：

Inductive relation : nat -> nat -> Prop :=
  | A : relation 1 2
  | B : relation 2 3.

报错信息：Error: The reference B was not found in the current environment.

• 多构造子示例2：

Inductive le : nat -> nat -> Prop :=
  | le_n (n : nat) : le n n
  | le_S (n m : nat) : le n m -> le n (S m).

报错信息：Error: The reference m was not found in the current environment.

使用环境：

The Coq Proof Assistant, version 8.18.0
compiled with OCaml 5.1.0

已尝试操作：将代码中的制表符替换为空格，未更换Coq版本（该版本数日前可正常编译）

解决思路 #

• 排查构造子格式问题：确保构造子之间的分隔符是单个竖线加空格，且每行代码无全角空格、非标准换行符等不可见字符。建议手动重新输入多构造子的代码，避免复制粘贴引入的格式异常。
• 排除上下文污染：在全新的Coq会话或空白文件中测试代码，排除当前环境中旧定义、命名冲突等因素的干扰。
• 验证OCaml版本兼容性：Coq 8.18.0官方推荐搭配OCaml 4.14.x版本，虽然支持OCaml 5.x，但OCaml 5.1.0可能存在未适配的语法解析问题。可尝试切换到OCaml 4.14.x重新编译Coq，观察问题是否消失。
• 检查编辑器插件影响：部分编辑器的Coq自动格式化插件可能错误修改代码结构，暂时禁用相关插件后手动编写代码测试。
• 重置Coq配置：若之前修改过~/.coqrc等配置文件，恢复为默认配置，排除自定义配置导致的解析异常。

内容的提问来源于stack exchange，提问作者Ulises Torrella