The Coq mailing list

[Alan Schmitt <alan.schmitt AT polytechnique.org>]

Hello,

I just noticed I had many broken links on my site that come from using
coqdoc with html output. More precisery, when I run

coqdoc -toc -html  -d html *.v

I get an html file for each of the .v files, as well as a toc.html and
index.html. In the later, I have a lot of links of the form:

<a href="agent.html#agent">agent</a> [inductive, in <a 
href="agent.html">agent</a>]<br/>

but no file "agent.html" was generated.

There is an agent target defined in one of the files:

HOC02DefLTS.html:<span class="id" type="keyword">Inductive</span> <a 
name="agent"><span class="id" type="inductive">agent</span></a> : <span 
class="id" type="keyword">Set</span> :=<br/>

but the file name is not correctly set in index.html.

Is it a (known) bug?

Thanks,

Alan