The Coq mailing list

[Makarius <makarius AT sketis.net>]

On Tue, 21 Apr 2009, Gyesik Lee wrote:

> on top of Debian Linux I am trying to use Coq 8.2.1 with Emacs 21.4.1
> plus Proof General.
> But it seems that Proof General 3.7.1 won't work with Coq 8.2.1.
> Is there a way to force it to work?

This is probably just one of the usual Proof General + Emacs 
incompatibilities, and Coq is innocent.  (The same happens for Isabelle 
Proof General all the time.)


> Or another option?

In the past I used to have a manually compiled versions of XEmacs 21.4.x, 
because the Debian / Ubuntu package never worked for me.  Now even that 
often fails, and I have switched to GNU Emacs 22 Gtk (on Ubuntu); it is 
probably the same for Debian.

In general, 21.x Emacsen are more likely to fail with newer Proof General 
versions.  Look for GNU (not X) Emacs and 22.x or 23.x.


        Makarius