参考信息在当前环境中找不到

Question

当我尝试在Adam Chlipala 在当前环境中找不到参考信息“ nofollow noreferrer”>带有依赖类型的认证编程下载软件CPDT捆绑包。该文件是 logicprog.v 第155行。在此之前还有其他问题（请参阅此处）。还有很多错误，我必须将[]更改为{}周围的东西。但这似乎是最后一个错误。

Answer 1

周围的文本提到 info 不再可用：

使用信息战术。 （截至撰写本文时，COQ 8.4中没有这种战术，但我希望它能尽快重新出现。特殊情况 info_auto tactic是作为自动的健谈替代品提供的。）

部分被命令替换 > ：

(* Instead of: info auto 6 *)
Info 1 auto 6.

另一种选择是仅删除 info ，然后跳过提到它。