The Coq mailing list

[Claude Marche <Claude.Marche AT lri.fr>]

Sorry, I misunderstood you question. I think the character 207A cause
pb but not 211A, because Coq recognizes only a part of unicode
characters. I suggest you report a bug, giving the set of characters you
would like to be supported.

- Claude

>>>>> "roconnor" == roconnor  
>>>>>Â <roconnor AT theorem.ca>
>>>>>  writes:

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

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

    roconnor> -- 
    roconnor> Russell O'Connor                                      
<http://r6.ca/>
    roconnor> ``All talk about `theft,''' the general counsel of the American 
Graphophone
    roconnor> Company wrote, ``is the merest claptrap, for there exists no 
property in
    roconnor> ideas musical, literary or artistic, except as defined by 
statute.''
    roconnor> --------------------------------------------------------
    roconnor> Bug reports: http://coq.inria.fr/bin/coq-bugs
    roconnor> Archives: http://pauillac.inria.fr/pipermail/coq-club
    roconnor>           http://pauillac.inria.fr/bin/wilma/coq-club
    roconnor> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

-- 
| Claude Marché           | 
mailto:Claude.Marche AT lri.fr
 |
| LRI - Bât. 490          | http://www.lri.fr/~marche/  ;|
| Université de Paris-Sud | phoneto: +33 1 69 15 64 85  |
| F-91405 ORSAY Cedex     | faxto: +33 1 69 15 65 86    |