The Coq mailing list

[Benjamin Werner <benjamin.werner AT inria.fr>]

With some emacs versions, this Coq/PG combination will only work
if PG  is in V8.1 mode. But when
one switches to V8.2, PG behaves as if it does not know how to handle  
8.2 and thus
falls back into 8.0 mode. On the Mac versions of emacs, this can break  
the undo
command for instance.

Try to add:

(setq coq-version-is-V8-1 t)


to your .emacs

Benjamin


Le 21 avr. 09 à 15:07, Makarius a écrit :

> 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
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>         http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club