The Coq mailing list

[Andrej Bauer <andrej.bauer AT andrej.com>]

What is the recommended way of getting coqdoc to pretty-print (in
LaTeX) symbols that were imported?

For example, suppose I define an operator 'cow' in A.v together with
coqdoc pretty-printing instruction on how it should be printed. If I
then Require Import A.v from B.v, coqdoc will not typeset cow prettily
when I run coqdoc on B.

With kind regards,

Andrej