The Coq mailing list

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

I noticed that utf8.v is part of coqide rather than being part of Coq.
Any reason for that?
After all, utf-8 encoding can be used with most editors nowadays.


        Stefan


PS: Better yet, why not recognize ∀ as a shorthand for "forall" in general
    so you don't need to enumerate the various different forms of forall you
    intend to use?  I.e. do it at the level of the lexer rather than in the
    camlp4 parsing.

PPS: the utf8.v file of 8.0pl1 has a bug: it uses ⌉ (i.e. right ceiling)
     rather than ¬ (i.e. not sign) for the the ~ negation.