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: Benoit Montagu <Benoit.Montagu AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] rules for which Unicode symbols may be used in notations
Date: Thu, 07 Oct 2010 21:47:27 +0200
Openpgp: url=http://gallium.inria.fr/~montagu/pgp_montagu.asc

> Concerning extraction, I suppose you refer to the lack of unicode name
> support in Ocaml ?
Yes.

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

-- Beno�t

Attachment: signature.asc
Description: OpenPGP digital signature

[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