The Coq mailing list

[Adam Megacz <megacz AT cs.berkeley.edu>]

The Unicode character range 0x1D2C through 0x1D50 contains superscripted
versions of the Latin alphabet (lower case).  These could be very useful
in notations -- for example, I wanted to create a superscripted "op" to
denote the opposite of a category, since I use contravariant functors
a lot.

Coq seems to react rather strangely to characters in this region.  It
will let me define a notation involving these characters, and will use
it correctly when pretty-printing.  However, if I attempt to use the
notation I have defined in a Gallina term, it will either go into an
infinite loop (100% CPU) and/or report a lexer error.

I tried to patch Coq to fix this, but the root cause seems to be the
tables in lib/unicodetable.ml which classify characters, and these
tables appear to have been machine-generated by some program which is
not part of Coq.  Is this true?  If so, are the rules governing the use
of Unicode characters beyond Coq's control?

My plan was to add a vernacular command to allow the user to classify or
reclassify character ranges, similar to what is done in TeX.

Obviously this is not a very important issue.

  - a