coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] coqdoc with multiple directories

From: Pat Castelnau <dfzone-coq AT yahoo.fr>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] coqdoc with multiple directories
Date: Sun, 8 Jun 2008 07:38:26 +0000 (GMT)
Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=s1024; d=yahoo.fr; h=Received:X-Mailer:Date:From:Reply-To:Subject:To:MIME-Version:Content-Type:Content-Transfer-Encoding:Message-ID; b=0jP3wBE6FSc/Ndytk/BZ6NpM6jIDBHSL+lD/mJctnsQoql9TSid5XF9Ef6gWCYgNsZFHyi4GchT9IpLXea/cmWaiL/aamWimgGZnH92c76mEpdfertgJktSLuxopuvEpDTlCQMwXgKuX7SgfChUnfY1P+uMvDqMJ/mxmv8WCKds=;
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

I have a file A.v that imports a library B which is in the file Dir/B.v. The
file A.html made by coqdoc has links to the standard library but not to my
library B. How can I tell coqdoc to make links to B? More generally, When a
development is split into different directories, what is the right way to use
coqdoc? Do I need to run coqdoc once per directory?

I use the svn version of Coq.

_____________________________________________________________________________
Envoyez avec Yahoo! Mail. Une boite mail plus intelligente
http://mail.yahoo.fr

[Coq-Club] coqdoc with multiple directories, Pat Castelnau