VSCode中Coq的Compute命令被蓝色下划线标注却无错误提示，求助

我无法理解为何在Visual Studio Code中，Coq代码里的Compute命令会被蓝色下划线标注，且没有任何相关错误提示。

Inductive day : Type :=
  | monday
  | tuesday
  | wednesday
  | thursday
  | friday
  | saturday
  | sunday.

Definition next_weekday (d:day) : day :=
  match d with
  | monday    => tuesday
  | tuesday   => wednesday
  | wednesday => thursday
  | thursday  => friday
  | friday    => monday
  | saturday  => monday
  | sunday    => monday
  end.

Compute (next_weekday friday).

Compute (next_weekday (next_weekday saturday)).

Example test_next_weekday:
  (next_weekday (next_weekday saturday)) = tuesday.

可能的原因及解决办法 #

• 扩展的视觉标记：VS Code中常用的Coq扩展（如Coqtail、Coq Language Server）会给Compute这类交互式命令添加蓝色下划线，这不是错误，只是用来区分命令和定义的视觉提示。如果觉得干扰，可进入扩展设置，查找“诊断”或“语法高亮”相关选项，调整标记规则。
• 未执行前置代码：Coq是增量式工具，需要逐步执行代码（比如选中代码按Ctrl+Enter）。如果Compute前面的Inductive和Definition还没被Coq处理，扩展会标记它处于未验证状态，但不会弹出错误。先执行完所有前置代码，下划线大概率会消失。
• 扩展版本兼容问题：旧版本的Coq扩展可能存在标记逻辑bug，建议在VS Code扩展市场中将Coq扩展更新到最新版本，再检查问题是否解决。
• 自定义配置干扰：查看工作区的.vscode/settings.json文件，若有自定义的Coq诊断配置，比如误开启了对交互式命令的检查，调整或删除相关配置项即可。

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