2
Software Foundations Coqの書籍（http://www.cis.upenn.edu/~bcpierce/sf/current/toc.html）を調べようとしていますが、Induction.v（http://www.cs.uml.edu/~rhenniga/coq/sf_induction.htmlのように見える）をコンパイルすると、メッセージ "Error：現在の環境で参照のevenbが見つかりませんでした。" - Basics.vのコンパイル後であっても。なぜどんなアイデア？Coqエラー：現在の環境で参照のevenbが見つかりませんでした
我々は間違っている可能性が何を知っているいくつかのより多くのコンテキストを必要としています。 CoqIDEを使用していますか？ Basics.vはInduction.vと同じディレクトリにありますか？コンパイルされたファイルBasics.voが実際にそのディレクトリに表示されていますか？ –
[この回答]（http://stackoverflow.com/a/16203673/596361）に従って、 'Induction.v'の先頭に' Add LoadPath "を追加してみてください。" –