如果我执行类似于-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的路径。我不知道(
(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.工作，那对我真的很有帮助。
建议通过opam-cf安装非系统版本的Coqhttps://coq.inria.fr/opam-using.html，主要是因为它方便了软件包(如mathcomp-*软件包(的安装，并且您可以一次专注于单个问题(coq vs emacs(
如果您仍然决定执行Coq和mathcomp的自定义安装，请不要忘记make install步骤，该步骤应该将编译的库文件复制到本地安装的子文件夹user-contrib/。
我注意到，在您的原始文章中，您的.emacs配置文件将"/usr/local/Cellar/coq/8.10.2_1/bin/coqtop"设置为coq-prog-name，而您的终端似乎使用/usr/local/bin/coqtop，这很可能是Coq的两个不同版本。因此，如果你使用这个编译和安装mathcomp，你就不会为另一个编译和安装它们。