The Coq mailing list

[Geoffrey Alan Washburn <geoffw AT cis.upenn.edu>]

Edsko de Vries wrote:

> I have a coq file (.v) with lots of unicode in it. When I try to generate the
> latex file using
>
> coqdoc --latex -g --inputenc utf8x stlu.v
>
> and then try to compile the Latex, I get
>
> ! Package utf8x Error: Malformed UTF-8 sequence.

I'm not sure about this.

> If I use the coqdoc --utf8 option instead, I get a similar error
>
> ! Package inputenc Error: Unicode char 
> \u8:ￜ\check@icr\expandafter
>  not
> set up f or use with LaTeX.
>
> Any ideas?

The above error message means that LaTeX does not know how to interpret 
the given Unicode glyph.  Some mappings are provided by default, but 
many Unicode glyphs are not given a default behavior.  Perhaps someone 
else has done something like this for the glyphs you are using. If not, 
for each glyph you need to define you will need to add a LaTeX commmand like

\DeclareUnicodeCharacter{03B1}{%my mapping for α%}

where the first argument is the hexadecimal identity of the Unicode 
glyph and the second argument is arbitrary LaTeX.  For example, I use

\DeclareUnicodeCharacter{03B1}{\textalpha}

where \textalpha is a macro that selects the α gylph from the 
appropriate font.