coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] rules for which Unicode symbols may be used in notations

From: Pierre Letouzey <Pierre.Letouzey AT pps.jussieu.fr>
To: Benoit Montagu <Benoit.Montagu AT inria.fr>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] rules for which Unicode symbols may be used in notations
Date: Fri, 8 Oct 2010 10:05:17 +0200

On Thu, Oct 07, 2010 at 09:47:27PM +0200, Benoit Montagu wrote:
> > Well, I recently enabled a translation from unicode
> > names to ascii ones. Produced names are ugly, but at least there're
> > accepted by Ocaml. More details here:
> >
> > http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2179
>
> Great! I guess I missed it in the (long) changelog for coq 8.3.
>

A good reason for that : I simply forgot to mention this new feature
there. This is fixed now, thanks for the remark...

Best,

Pierre

[Coq-Club] rules for which Unicode symbols may be used in notations, Adam Megacz
- Re: [Coq-Club] rules for which Unicode symbols may be used in notations, Benjamin C. Pierce
  - Re: [Coq-Club] rules for which Unicode symbols may be used in notations, David MENTRE
- Message not available
  - Re: [Coq-Club] rules for which Unicode symbols may be used in notations, Beno�t Montagu
    - Re: [Coq-Club] rules for which Unicode symbols may be used in notations, Christian Doczkal
    - Re: [Coq-Club] rules for which Unicode symbols may be used in notations, Benjamin C. Pierce
      - Re: [Coq-Club] rules for which Unicode symbols may be used in notations, Pierre Letouzey
      - Message not available
        
        Re: [Coq-Club] rules for which Unicode symbols may be used in notations, Benoit Montagu
        
        Re: [Coq-Club] rules for which Unicode symbols may be used in notations, Pierre Letouzey
- <Possible follow-ups>
- Re: [Coq-Club] rules for which Unicode symbols may be used in notations, Hugo Herbelin