The Coq mailing list

[Stefan Monnier <monnier AT iro.umontreal.ca>]

>> As far as I know, coq does not support the \uXXXX escape sequences,
>> but CoqIDE allows to input them directly : type CONTROL+SHIFT+211A and
>> you will see a marvellous bold math Q (if the font supports it...)

> Sorry I should have been more clear.  I've entered these characters
> together with ctrl+shift as you say.  The notation is accepted, but you
> cannot use it.  Coq seems to refuse to allow two unicode charaters to make
> one token.  Maybe it is a CamlP4 thing.

I've had similar problems but even with just single-unicode-char tokens.
E.g. I had no problem making notations using λ, Λ, ∀, 〈, or 〉 but couldn't
get Coq to accept ▷ or ▹.

I suspect the problem is that Coq doesn't actually understand utf-8 and so
some utf-8 sequences happen to only use octets considered as
symbol-constituents whereas others are less lucky.  This assumes that Coq
does not consider all octets 128-255 as symbol-constituents (maybe because
it assumes those octets are latin-1 chars or invalid control chars (for
128-159)).


        Stefan