The Coq mailing list

[Robert Rand <rrand AT seas.upenn.edu>]

For anyone else running into this problem, there is a -Q option that can be passed to coqdoc (corresponding to the -Q option in coqc): This is shown if you run Coqdoc --help but it isn't in Coq's online documentation. 

On Mon, May 6, 2019 at 4:06 PM Robert Rand <rrand AT seas.upenn.edu> wrote:

Hi,

I'm trying to compile coq to HTML using coqdoc but all the links in the index are broken. To be precise, they all go to VQC.[name].html#[lemma_name] (where VQC is the library name given in the _CoqProject) which doesn't exist. [name].html#[lemma_name] exists, but it doesn't take me to the right place in the file.

The command I'm using is

coqdoc -html --utf8 --coqlib http://coq.inria.fr/library/ --parse-comments --index coqindex --toc --toc-depth 2 --lib-name "" --lib-subtitles *.v

though I've tried a variety of flags.

Any idea how to fix this?

Thanks,

Robert