The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT pps.jussieu.fr>]

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ḱ
> >>
> >>
> >>
> >
> >