问Coq:错误:找不到库Coq.extraction.Extraction
EN

Stack Overflow用户

提问于 2019-05-18 21:57:24

回答 1查看 535关注 0票数 0

我正在选修“软件基础”课程。无法运行“提取”章节。在第一行Require Coq.extraction.Extraction.失败，并显示消息Coq: Error: Unable to locate library Coq.extraction.Extraction.

我正在CoqIde中运行它。

coqc -v: Coq证明助手，版本8.6 ( 2017年10月)，使用OCaml 4.05.0编译于2017年10月28日14:23:55

CoqIde版本: 8.6

CoqTop参数：-Q /home/evgenii/mysource/coq/coq-excercise/ LF LF

我遗漏了什么？

回答已采纳

发布于 2019-05-18 22:36:42

尝试将该行替换为Require Extraction. (Coq.extraction.Extraction似乎是一种向后不兼容的形式。)

8.6版本相当旧，所以如果它与您的Software Foundation发行版使用的版本不匹配，那么您可能会遇到其他兼容性问题。在Preface.v中查看预期的Coq版本，如果存在不匹配，请考虑升级。

票数 2

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/56199634

复制

相似问题

问Coq:错误:找不到库Coq.extraction.ExtractionEN