The Coq mailing list

[roconnor AT theorem.ca]

On Thu, 26 May 2005, Claude Marche wrote:

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

-- 
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''