coq - 部分 Coq 标准库无法加载

Question

我最近在我的系统上安装了 coq（首先来自 arch 用户存储库，然后通过 opam，面临同样的问题）。当我想试用标准库时，我意识到有些库可以加载，而有些则不能。例如

Require Import Arith.
Require Import Logic.

效果很好，而

Require Import Lists.

或者

Require Import Sets.

导致消息

Unable to locate library Lists.

这里可能是什么问题？

标签： coq