The Coq mailing list

[Benjamin Pierce <bcpierce AT cis.upenn.edu>]

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...)

    - Benjamin


On Feb 23, 2010, at 6:12 AM, Pierre Letouzey wrote:

> On Tue, Feb 23, 2010 at 12:03:42PM +0100, Bas Spitters wrote:
> > This approach would clutter the name space.
> > It would be better to change extraction mechanism.
> >
> > Best,
> >
> > Bas
>
> Well, it would be better to change ocaml to allow unicode identifiers.
> But since this is quite unlikely to happen anytime soon, I indeed plan
> to do some name mangling at extraction time. Won't be pretty, but if
> it helps...
>
> Regards,
>
> Pierre
>
>
> > On Tue, Feb 23, 2010 at 10:53 AM, Pierre Courtieu
> > <Pierre.Courtieu AT cnam.fr>
> >  wrote:
> > > I suppose that using unicode only in notations is a way to work  
> > > around
> > > this limitation of ocaml.
> > > Cheers,
> > > Pierre Courtieu
> > >
> > > 2010/2/22 Danko Ilik 
> > > <dankoilik AT gmail.com>:
> > > > I forward the e-mail that was meant to go to coq-club:
> > > >
> > > > > From: Bas Spitters 
> > > > > <spitters AT cs.ru.nl>
> > > > > Date: February 22, 2010 4:39:42 PM GMT+01:00
> > > > > To: Danko Ilik 
> > > > > <dankoilik AT gmail.com>
> > > > > Subject: Re: [Coq-Club] Unicode input
> > > > >
> > > > > It seems that haskell does support unicode, but there are some
> > > > > problems with lambdas:
> > > > >
> > > > > http://hackage.haskell.org/trac/ghc/ticket/1102
> > > > >
> > > > > Pierre: Does switching to unicode mean that we will have to give  
> > > > > up extraction??
> > > > >
> > > > > Best,
> > > > >
> > > > > Bas
> > > >
> > > > --
> > > > Danko Iliḱ