The Coq mailing list

[Benedikt Ahrens <benedikt.ahrens AT gmx.net>]

Hello,

I have a Coq library that uses Unicode notation and identifiers, and I
am trying to produce latex documentation for this library, for inclusion
in an article.

The coqdoc tool with --latex option seems to work better than anything
else I have seen so far, and its output mostly compiles with pdflatex.
However, I am getting a few errors of several different kinds, examples
of which I post at the bottom of this email.

I would be grateful for any hints on how to patch coqdoc to remedy (some
of) these errors.

Alternatively, I would also be grateful for pointers to other tools that
allow the creation of latex code from Coq files containing Unicode. It
is important that the code can be compiled with pdflatex.

The coqdoc version used is from commit 76d6a8c (branch v8.5).
The texlive packages are the ones shipped in Debian 8. I can give more
precise information if necessary, of course.


Thanks a lot.
Best,
Benedikt


a)

! LaTeX Error: Command \textmu unavailable in encoding T1.

See the LaTeX manual or LaTeX Companion for explanation.
Type  H <return>  for immediate help.
 ...

l.621 ...s alt.xCExBC 0}{\coqdocdefinition{μ\_0}}


b)

! Undefined control sequence.
\u-default-964 #1->\texttau

l.457 ...84 LamE algebra on Lam}{\coqdoclemma{τ}}


c)

! Undefined control sequence.
<argument> \rrbracket

l.372 ... ',' x 'xE2x9FxA7'}{\coqdocnotation{⟧}}


d)

! Package ucs Error: Unknown Unicode character 10627 = U+2983,
(ucs)                possibly declared in uni-41.def.
(ucs)                Type H to see if it is available with options.

See the ucs package documentation for explanation.
Type  H <return>  for immediate help.
 ...

l.533 \coqdockw{Local} \coqdockw{Notation} "⦃
                                                f ⦄" :=
(\coqref{SubstSyst...

? H
Unicode character 10627 = U+2983:
LEFT WHITE CURLY BRACKET
Character is not defined in uni-*.def files.
Enter I!<RET> to define the glyph.
?