The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

Furher to my previous bugreport,

> I suspect it's a bug in coqdoc.  When I run a UTF8 validity tester
> over the .tex file generated by coqdoc, it reports loads of malformed
> UTF8 sequences.
> 
> I think they are all due to the same problem. Here's a line with such
> a malformed sequence:
> 
> \coqdockw{Notation} "\coqdocid{<E2>}<80><A2>" :=
> \coqdocid{Unique}.\coqdoceol
> 
> where I've replaced the UTF8 sequence with their ASCII codes for
> clarity. The sequence <E2><80><A2> corresponds to the unicode 0x2202
> (I think), but the problem is clear: the closing curly is in the
> middle of the sequence! It should read
> 
> \coqdockw{Notation} "\coqdocid{<E2><80><A2>}" :=
> \coqdocid{Unique}.\coqdoceol
> 
> If I manually fix those curlies (and insert the
> DeclareUnicodeCharacter statements), everything works.

Here is a small script that fixes these errors. If I run this script
over the file generated by coqdoc, everything works:

#!/bin/bash
perl -pi -e "s/([\x80-\xFF])}([\x80-\xFF]+)/\1\2}/g" $1

May be useful to someone.

Edsko