The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

Hi,

Feel free to open an issue about this lack of documentation at
https://github.com/coq/coq/issues.
If you see how to fix the doc, you may also open a pull request directly.

Thanks,
Théo

Le mar. 7 mai 2019 à 17:56, Robert Rand 
<rrand AT seas.upenn.edu>
 a écrit :
>
> 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