The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi Andrej,

> 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.

Actually, coqdoc needs all files together in the correct order of
dependencies so that pretty-printing instructions in one file are
available to the next files (there is no notion of A.something
compiled coqdoc file such that B.v knows what printing instructions
are in A.v, and no export of the printing instructions to A.vo
either).

Otherwise said, "coqdoc A.v B.v" will work.

Hugo