The Coq mailing list

[Fr�d�ric Besson <fbesson AT irisa.fr>]

Le 23 févr. 10, à 15:36, Benjamin Pierce a écrit:

> Since we're talking about unicode, may I ask if people are  
> successfully using unicode notations with proof general and emacs  
> 22.0?  For me, the notations display correctly in the .v buffer,  
> but display as ? in the goals and responses buffers.
>
> (I see that newer PG releases use a different mechanism for  
> displaying unicode, but this requires upgrading to emacs 23, which  
> is not installed everywhere yet and indeed doesn't completely work  
> on my machine yet, for reasons yet to be diagnosed...)
For me, unicode works with the following configuration:
- GNU Emacs 22.2.1 (i386-apple-darwin8.11.1, Carbon Version 1.6.0) --  
not quite 22.0 but not 23
coq-prog-args set to ("-emacs-U")
- Proof General Version 3.7.1.1
- Coq 8.2pl1

--
Frédéric Besson