Link "X" not found in current environment

Question

I use CoqIDE to do the exercises in the Software Foundations book about Coq. I can successfully compile Basics.v, leaving Basics.vo and Basics.glob in my directory. When I try to start Induction.v, it works. When I try to compile it, it complains about tons of missing links like evenb and negb_involutive . If I copy the contents of Basics.v to Induction.v, it compiles, but obviously this is not the way to go.

This is not a duplicate of the question . Coq error: the reference four was not found in the current environment , since I already did this:

Compile Basics.v. Check if the basics.vo file is in the directory. Now compile Induction.v. This last step failed.

Answer 1

I myself experienced this error. Try opening CoqIDE from the same directory as the Software Foundations files, and compile it. If you are working on Linux, just open a terminal, go to this directory and enter coqide there. I do not quite understand how to do this on other systems, for example. Mac OS, but I noticed that only opening the application through the icon makes it fail.