Search code examples
argumentscoqimplicit-typing

Coq --- Arguments directive

I am reading Software foundations book and I came across a command that declares parameters as implicit:

Arguments nil {X}.

where, for example:

Inductive list (X:Type) : Type :=
| nil : list X
| cons : X -> list X -> list X.

However, whenever I try to execute such commands I get the following message:

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

The same message appears even if I try to compile scripts that come with the book. What could be the problem?

I am using Coq version 8.3pl4 and CoqIDE editor.

Solution

  • I just tried it on my (somewhat old) Coq 8.4 and I don't have any problem with the implicit declaration. However if I write Argument instead of Arguments (notice the lack of "s"), I get 

    Error: Unknown command of the non proof-editing mode.

    Did you correctly spelled it ?

    EDIT: sorry, I miss-read your version. It seems that the Arguments command has been added post 8.4 (it does not appear here but appears here. I advise you update your Coq version if possible, or restrict to using 8.3 Implicit related commands (wild guess: Implicit Arguments foo.)