coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq 8.3 + Proofgeneral + Unicode

From: Pierre Courtieu <Pierre.Courtieu AT cnam.fr>
To: Paolo Herms <paolo.herms AT cea.fr>
Cc: coq-club AT inria.fr, AUGER <Cedric.Auger AT lri.fr>
Subject: Re: [Coq-Club] Coq 8.3 + Proofgeneral + Unicode
Date: Tue, 30 Mar 2010 17:27:50 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:from:date :x-google-sender-auth:message-id:subject:to:cc:content-type; b=k8q+nWNSOJCpqmU5KQdw9MLo01iFQ8NB1CWwXWUu+wNMu4iZQq+fKIWk8vHuzwH3FZ jnY7YrW1+0sSIG6xQ1c/Wi+1rleNfnVituHyVrzXjkEXpzWWGCqEre7TwkxVSJDnO4Ms lw3A2ijYvrVDO6IuWSxGDoIk/f4P9CI7th6q0=

Hello, this was a bug of PG due to a change in the error "ascii
underlining" of 8.3beta. Thanks for reporting.

This has been fixed with the help of Hugo in coq + pg. However
updating only pg to current cvs should make things better with
coq-8.3beta, though underlining should be less accurate with utf8.

Best regards,
Pierre Courtieu

2010/3/29 Paolo Herms
<paolo.herms AT cea.fr>:
> On Monday 29 March 2010 13:06:20 AUGER wrote:
>> Have you tried with 8.2, and your bug is 8.3 specific?
>
> With coq 8.2 the problem does not occur on the same machine, so I rule out
> font or configuration problems.
> --
> Paolo Herms
> PhD Student - CEA-LIST Software Safety Lab. / INRIA ProVal Project
> Paris, France
>
>

[Coq-Club] Coq 8.3 + Proofgeneral + Unicode, Paolo Herms
- Re: [Coq-Club] Coq 8.3 + Proofgeneral + Unicode, Paolo Herms
  - Re: [Coq-Club] Coq 8.3 + Proofgeneral + Unicode, Pierre Courtieu