Некоторая часть стандартной библиотеки Coq не может быть загружена - PullRequest
0 голосов
/ 06 июля 2018

Я недавно установил coq в своей системе (сначала из пользовательского репозитория arch, но затем через opam, столкнувшись с той же проблемой). Когда я захотел опробовать стандартную библиотеку, я понял, что некоторые библиотеки можно загрузить, а другие нет. Например

Require Import Arith.
Require Import Logic.

работает просто отлично, тогда как

Require Import Lists.

или

Require Import Sets.

результаты в сообщении

Unable to locate library Lists.

В чем здесь проблема?

...