Если я сделаю что-то вроде - From mathcomp Require Import ssreflect., это выдаст мне следующую ошибку.
Error: Cannot load mathcomp.ssreflect.ssreflect: no physical path bound to
mathcomp.ssreflect
Но если я сделаю это вместо - Require Import ssreflect. Это скомпилируется просто отлично. Вероятно, это потому, что у меня установлен ssreflect, но не совсем так, как я хочу.
Но дело в том, что я хочу первый способ работы, потому что у меня много программ, написанных таким образом, а это не так кажется логичным изменить строку в каждом из них.
Это то, что у меня есть в моем файле .emacs - (я думаю, может быть, мне нужно добавить что-то вроде пути к mathcomp / ssreflect .. I не знаю)
(load "~/.emacs.d/lisp/PG/generic/proof-site")
(custom-set-variables
;; custom-set-variables was added by Custom.
;; If you edit it by hand, you could mess it up, so be careful.
;; Your init file should contain only one such instance.
;; If there is more than one, they won't work right.
'(coq-prog-name "/usr/local/Cellar/coq/8.10.2_1/bin/coqtop")
'(package-selected-packages (quote (company-coq)))
'(proof-three-window-enable t))
;; Load company-coq when opening Coq files
(add-hook 'coq-mode-hook #'company-coq-mode)
Было бы очень полезно, если бы кто-нибудь помог мне заставить From mathcomp Require Import ssreflect. работать.