The Coq mailing list

[Jean-Marc Notin <notin AT lix.polytechnique.fr>]

Hello,

> I am using coq  8.1pl3 and I have a hard time using coqdoc
> for latex (or even html) output.
>
> I have attached a very short example and I wonder if there is
> something wrong somewhere (wrt. coqdoc).
> When I run:
> coqdoc --latex -g test.v
>
> In the generated test.tex file, the second (** special comment
> is not interpreted correctly. This is a silly example but I have
> the same problem in a few "real" modules I am working on.
> Sometimes the output is simply an empty latex or html document.
> Strangely enough, other modules are processed correctly and
> I do not understand why.
>
> Is there something wrong with my example or do I have to fill a
> coq-bug report ? (maybe I should first try 8.2).
The file you provided is a DOS file (ie lines end up with CRLF) and 
coqdoc seems to have trouble with it. Using 'dos2unix' solves the problem.

--
Jean-Marc Notin
CNRS - LIX

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature