Basics.vo содержит основы библиотеки, а не библиотеку Metalib.Basics
Я получаю ошибку "Basics.vo содержит основы библиотеки, а не библиотеку Metalib.Basics" в CoqIDE 4.5. Я следую Основам программного обеспечения и импортирую Основы как "Требуются Основы экспорта". Также я скомпилировал основы, используя тот же CoqIDE. В прошлом я использовал CoqIDE 4.2, и это хорошо работало в CoqIDE 4.2. Теперь я переключился на CoqIDE 4.5, удалил ранее скомпилированный Basics.vo и скомпилировал снова. Может кто-нибудь помочь мне в этом?
Я попытался удалить ранее скомпилированный Basics.v. Также попытался перезапустить CoqIDE несколько раз.
Print LoadPath.
Require Export Basics.
Theorem plus_n_O_firsttry : forall n:nat, n = n+0.
Proof.
intros n.
simpl.
Abort.