CoqIDE を実行して教科書シリーズ「ソフトウェアの基礎」を読んでいます。現在、「論理的な基礎」を読んでいます。2章(誘導編)を始めたばかりですが、ラインを走らせようとすると
From LF Require Import Basics.
エラーステートメントが表示されます
The file ...\LF\Basics.vo contains library
Basics and not library LF.Basics
ファイルが置かれているディレクトリの名前を変更して、バッファを再コンパイルしようとしましたが、これらのアクションはどちらも役に立ちませんでした。この問題を解決するにはどうすればよいですか?