coq - Basics.vo 包含库 Basics 而不是库 Metalib.Basics

Question

我在 CoqIDE 4.5 中收到错误“Basics.vo 包含库 Basics 而不是库 Metalib.Basics”。我正在关注软件基础并将基础知识导入为“需要导出基础知识。”。我还使用相同的 CoqIDE 编译了 Basics。过去我使用的是 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.