Пакет для coq странных файлов порядка отсутствует в mathcomp?
Я установил coq через opam на Ubuntu 14.04. Я пытаюсь получить (и в конечном итоге запустить) исходный код для "раздетого" доказательства теоремы о нечетном порядке; а именно файл stripped_odd_order_theorem.v, Вот больше на моей установке:
$ coqtop -v
The Coq Proof Assistant, version 8.4pl6 (June 2017)
compiled on Jun 14 2017 12:32:33 with OCaml 4.02.3
Команды как
opam install coq-mathcomp-solvable
работает нормально, но я ищу файл stripped_odd_order_theorem.v, которая была у меня в ранней версии ssreflect, когда у меня был установлен coq другим способом. Согласно coq.io этот файл теперь, кажется, живет в пакете coq-mathcomp-odd-order но
$ opam install coq-mathcomp-odd-order
[ERROR] No package named coq-mathcomp-odd-order found.
Я не понимаю