公司费用 Proof General的Coq模式扩展集的集合。 请参阅下面的,或直接跳至并在尝试使用Mx company-coq-tutorial的教程! 建立 梅尔帕 proof-general和company-coq都在 (Emacs软件包的存储库)上。 如果您已经使用MELPA,请跳过此步骤。 否则,将以下内容添加到您的.emacs然后重新启动Emacs: ( require 'package ) ( add-to-list 'package-archives '( " melpa " . " https://melpa.org/packages/ " ) t ) ( packag