The Coq mailing list

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

> > Try giving the --gallina (or -g for short) flag to coqdoc.  That  
> > should do what you want here.
> 
> Thanks for the quick reply. However, when I specify -g, definitions and
> fixpoints disappear along with the proofs.

Right, after some experimenting it turns out that coqdoc is thrown off
by the presence of non-Unix style line endings; when I run 

  coqdoc -g Proofs.v --latex && latex Proofs.tex

all sorts of stuff is missing from the output, but then when I run

  dos2unix Proofs.v

and re-generate the .tex file, everything works as expected.

Running gallina *does* work without converting line endings first. 

Thanks for the help,

Edsko