Coq "Error: No focused proof" when using "Arguments" command

Question

I am working through the Software Foundations book. In the chapter on polymorphism, there is a section on "Implicit Arguments". In this section, there is the line:

Arguments nil {X}.

When I try to run Coq on the Poly.v file (the source for the chapter, available in this tarball), it stops at the above line, giving me the error:

Error: No focused proof (No proof-editing in progress).

I have reduced the Poly.v file down to just these contents, which still give the same error:

Inductive list (X:Type) : Type :=
  | nil : list X.

Arguments nil {X}.

The only thing I can find in the Coq reference manual on this error is

When one attempts to use a proof editing command out of the proof editing mode, Coq raises the error message : No focused proof.

I think "proof editing mode" refers to the context where a theorem is being proven using tactics. I do not think it is in that mode, and nor does Coq, since it says "No proof-editing in progress". So that makes sense.

The error claims that Arguments is a "proof editing command", though it doesn't say that in its documentation, and Arguments is not mentioned in the chapter on proof handling.

This leads me to think that Coq is incorrectly treating Arguments as a proof-editing command, but I don't know why.

I assume this must be something wrong with my setup rather than the Poly.v file itself, since it's part of the Software Foundations book. I am using CoqIDE, as part of Coq 8.3pl4, distributed with Ubuntu 12.04.

Answer 1

This is an issue with the version of coq you are using. The current edition of Software Foundations is only compatible with coq 8.4. If you'd like to continue without upgrading coq, the old version of the relevant command is:

Implicit Arguments nil [[X]].

You can find a complete copy of poly.v that is compatible with your version of coq here:

http://www.seas.upenn.edu/~cis500/cis500-s13/sf/Poly.html

Have fun!