主要参考https://wiki.ccs.neu.edu/display/~vkoutav/Coq-ProofGeneral-Emacs-Windows

文章中有些链接失效了

容易出错的地方说明下

%COQBIN%\coqtop.opt.exe -top "%COQTOP%" -emacs-U

在该目录下没有找到

coqtop.opt.exe

只有
coqtop.exe
修改之

对于Run Emacs, open your .emacs file (C-X C-F ~/.emacs), and add the following two lines to it, 这一步
请搜索emacs.d文件夹，Win7和XP位置不同，在该文件夹下建立init.el文件，

init.el文件里填入
(defvar coq-prog-name "C:/Program Files/Coq/bin/coq-emacs.bat")

(load-file "G:/develop/ProofGeneral-4.2pre/ProofGeneral-4.2pre120206/generic/proof-site.el")
当然要改成你对应的路径
然后直接启动
emacs
就ok了
以下是参考原文


Installation How-To for Coq + ProofGeneral + GNU Emacs + Windows

This is how I made Coq, Proof-General, Emacs, and Windows work all together. I describe my own situation, giving the version numbers of the programs I used, and the directories I've installed them in. I suppose you can install newer versions in different directories

 and things will still work. If you do that some renaming is necesary.


GNU Emacs:



If you have a recent version of GNU Emacs running (22.1 or later) then skip this section.

Download the latest version of GNU Emacs for windows. I used version 22.1.0.0.

Unzip the the installation zip, and copy it somewhere on you disk (e.g. C:\Program Files\Emacs\emacs-22.1).

Run the program C:\Program Files\Emacs\emacs-22.1\bin\addpm.exe to create a Start Menu item for emacs.



Coq:



Download the latest version of Coq (8.1pl2, Oct. 2007)

Install Coq in a local directory of your choice (e.g. C:\Program Files\Coq)

You now have to make a .bat file that sets the right environment variables when calling Coq from within emacs, and passes the right command-line arguments to it. Create somewhere in your emacs's exec-path (typically someplace like C:/Program Files/Emacs/emacs-21.2/bin/)

 a file called 'coq-emacs.bat' that contains the following:



@echo off
set COQTOP=C:\PROGRA~1\Coq
set COQLIB=%COQTOP%\lib
set COQBIN=%COQTOP%\bin
set PATH=%PATH%;%COQBIN%
set HOME=%HOMEPATH%
%COQBIN%\coqtop.opt.exe -top "%COQTOP%" -emacs-U







ProofGeneral:



Download the development release of ProofGeneral (3.7pre071025). In Windows, GNU Emacs communicates with the Coq

 process in unicode, but the stable release of ProofGeneral (3.5) can't handle unicode and hangs.

Install ProofGeneral in a local directory of your choice (e.g. C:\Program Files\Proofgeneral-3.7pre071025)

Make sure that there are no .elc files in C:\Program Files\Proofgeneral-3.7pre071025 and its sub-directories; the development release shouldn't have any, but if it does then just delete them.

Run Emacs, open your .emacs file (C-X C-F ~/.emacs), and add the following two lines to it, in this order:



(defvar coq-prog-name "coq-emacs.bat")
(load-file "C:/Program Files/ProofGeneral-3.7pre071025/generic/proof-site.el")








Things should work now. If you fire up emacs and open a test.v file, you should see ProofGeneral's welcone buffer. Then write something trivial:


Definition A:Set.




and press "C-C C-n". The above line should be underlined and the following should appear in the *goals* buffer:


1 subgoal
  
  ============================
   Set




(Thanks to Mitch Wand for debugging this how-to and suggesting a better Emacs configuration than I initially had.)