The Coq mailing list

["Michiel Helvensteijn" <mhelvens AT gmail.com>]

Hi!

Quick introduction: I'm a PhD student in Computer Science and I've been
learning Coq for a couple of weeks now. I'm quite impressed and looking
forward to using it more. I'm planning to encode the theory of my PhD thesis
in Coq, so I'll probably have some questions in the coming months. I regret
that my first question to the list is so superficial, but:

I just found the symbols I'm using for my lattice structure in unicode. They
are:

'OR WITH DOT INSIDE' (U+27C7)
'AND WITH DOT' (U+27D1)

Surprisingly, Coq is fine with the latter, but produces a warning for the
former: "Token '...' contains unicode character 0x27c7 which will not be
parsable."

Since they both belong to the same block, I suspect a bug. I tried to fix it
myself, but I'm not that good with OCaml yet. 'lexer.ml4', somewhere in
'lookup_utf8_tail', right? But that's as far as I got.

Could this be fixed in the repository? Also (depending on how long that
takes), could someone tell me how to fix it myself?

Some useful links:

http://www.fileformat.info/info/unicode/char/27c7/index.htm
http://www.fileformat.info/info/unicode/char/27d1/index.htm

Thanks in advance!

--
www.mhelvens.net