Basics.vo содержит основы библиотеки, а не библиотеку Metalib.Basics - PullRequest
Новая
       33

Basics.vo содержит основы библиотеки, а не библиотеку Metalib.Basics

0 голосов
/ 13 февраля 2019

Я получаю ошибку "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.
...