coqdoc --html does not work properly when invoked from a parent folder

[coqbot]

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#2366
From: @erikmd
Reported version: 8.2
CC: @herbelin, @glondu

[coqbot]

Comment author: @erikmd

When I execute for instance the command:

$ coqdoc -toc -html -d html theories/*.v

(or a similar one invoked by a Coq Makefile),
the generated HTML files are of lower quality than by doing sth like

$ cd theories && coqdoc -toc -html -d html *.v

More precisely,

1. all identifiers are preceded by <span class="id" type="var">,
   whenever is their real type (section, lemma, tactic, etc.),
   thus the HTML files do not respect the color code any more;
2. moreover, these files do not contain any more hyperlink tags
   <a name="..."> nor <a class="idref" href="...">;
3. and in the generated index.html file, all links are broken
   (except the last few links of the Library Index), i.e.
   the filename prefix "theories." corresponding to the
   folder at stake is missing.

This is reproducible with 8.2pl2.

Kind regards,
Erik.

[coqbot]

Comment author: @glondu

When I execute for instance the command:
$ coqdoc -toc -html -d html theories/*.v
(or a similar one invoked by a Coq Makefile),
the generated HTML files are of lower quality than by doing sth like
$ cd theories && coqdoc -toc -html -d html *.v

This and bug BZ#2363 make me think that coqdoc should accept a {make,tar}-style "-C" option.