【发布时间】：2013-12-02 03:29:25
【问题描述】：
我正在阅读Software Foundations 这本书。在the chapter on polymorphism 中有一个关于“隐式参数”的部分。在本节中，有一行：
Arguments nil {X}.
当我尝试在 Poly.v 文件（本章的源代码，this tarball 中提供）上运行 Coq 时，它停在上面的行，给我错误：
Error: No focused proof (No proof-editing in progress).
我已将 Poly.v 文件缩减为仅这些内容，但仍然出现相同的错误：
Inductive list (X:Type) : Type :=
| nil : list X.
Arguments nil {X}.
我在Coq reference manual 中唯一能找到的关于这个错误的是
当尝试在校样编辑模式之外使用校样编辑命令时，Coq 会引发错误消息：没有焦点校样。
我认为“证明编辑模式”是指使用策略证明定理的上下文。我不认为它处于那种模式，Coq 也不是，因为它说“没有正在进行校对编辑”。所以这是有道理的。
该错误声称Arguments 是一个“校样编辑命令”，尽管它在its documentation 中没有说，并且Arguments 在the chapter on proof handling 中没有提到。
这让我认为 Coq 错误地将 Arguments 视为校对编辑命令，但我不知道为什么。
我认为这一定是我的设置有问题，而不是 Poly.v 文件本身，因为它是软件基础书的一部分。我正在使用 CoqIDE，作为 Coq 8.3pl4 的一部分，随 Ubuntu 12.04 一起分发。
【问题讨论】：
标签： compiler-errors arguments coq proof