Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Coq 8.2.1 and Proof General 3.7.1 are compatible?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq 8.2.1 and Proof General 3.7.1 are compatible?


chronological Thread 
  • From: Gyesik Lee <gslee AT ropas.snu.ac.kr>
  • To: Pierre Courtieu <Pierre.Courtieu AT cnam.fr>
  • Cc: Benjamin Werner <benjamin.werner AT inria.fr>, Makarius <makarius AT sketis.net>, coq-club <coq-club AT pauillac.inria.fr>
  • Subject: Re: [Coq-Club] Coq 8.2.1 and Proof General 3.7.1 are compatible?
  • Date: Thu, 23 Apr 2009 10:54:17 +0900
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:date :x-google-sender-auth:message-id:subject:from:to:cc:content-type :content-transfer-encoding; b=Be8olXUuLCGOnkdA2DPOrXkvg3ztZaA0w208J55OVVErqjWFrGhzD6fiipU4QAcTkS OF34H8X2tpqt+hhOKTNIClZhNGb6z6ncGLF4VN5E1OBCYWtUGU68x9h0R/2hbq3//zMu lGZr4QUtJroRfF2eBiTS7/xLVIVivLaS0UM4I=
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hi,

many thanks for your help.
As many people said, I believe, Emacs 21.4 is a bit too old to support
all the functions of PG 3.7.1.
(I saw even that the next version of PG will not support Emacs 21 any more.)

>> Try to add:
>>
>> (setq coq-version-is-V8-1 t)
>
> This cannot hurt anyway, but it should generally not be necessary
> unless you deal with several versions of coq.

Indeed I tried without adding this line. The same thing happens.
PG works when Emacs21.4 is already started up.
However, not all the functions work.
For example, the syntax highlighting doesn't work and a bit different
message in "Message"

coq version is 8.2: proofgeneral is in coq 8.1 mode (to force another
version, see for example C-h v `coq-version-is-V8-0)'

> Please consider submit a bug report on 
> http://proofgeneral.inf.ed.ac.uk/trac/wiki.

Yes, I will.

Gyesik



Archive powered by MhonArc 2.6.16.

Top of Page