Coq + Emacs? ``Check`` can't see what is defined in the source file

Question

So I am playing with Coq using Emacs as the IDE. Both proof-general and company-coq are installed and load correctly.

Then I open dummy whatever_name.v file and define recursive function using the Fixpoint keyword.

Then I run coq-Check on it and get:

> Check addnm .

Error: The reference addnm was not found in the current environment.

However, for example, Inductive unit : Set := tt. works perfectly well.

What am I doing wrong?

Answer 1

I have the impression you did not ask Coq to read the addnm definition. Try pressing C-c C-n on your Coq buffer. This should instruct Proof General to send in the next command to Coq for processing. You should see your buffer progressively turning a different color as the commands are sent. Once the definition of addnm is highlighted, you should be able to check it (C-c C-a C-c).

(The reason unit still works is that its definition is automatically loaded when you start Coq in Emacs.)