The Coq mailing list

[Fr�d�ric Peschanski <Frederic.Peschanski AT lip6.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).

Cheers,
Frederic.

(** * a section about sets

bla bla 1

*)

Section sets_module.

(** ** Basic definitions 

Bla bla 2

*)

Inductive set (Elem:Set) (Elemeq_dec: forall e1 e2 : Elem, { e1 = e2 } + { e1 
<> e2 }) : Set :=
| empty: set Elem Elemeq_dec
| elem: Elem -> set Elem Elemeq_dec -> set  Elem Elemeq_dec.

End sets_module.