The Coq mailing list

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

Hi Alan,

You probably mean the same bug as identified in
https://coq.inria.fr/bugs/show_bug.cgi?id=2914. This is 
fixed in 8.4pl1. Sorry for this unfortunate regression
of coqdoc.

Best,

Hugo

On Fri, Jan 04, 2013 at 11:32:57AM +0100, Alan Schmitt wrote:
> 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