The Coq mailing list

[Jasper Stein <jasper AT cs.kun.nl>]

Jean-Christophe Filliatre wrote:

> Remarque : il n'y a même plus lieu de respecter un certain ordre entre
> les répertoires. Seul l'ordre  entre les fichiers, calculé par coqdep,
> est pris en compte par make.

Aussi, il y a la possibilite d'avoir des fichiers dependants sur une 
autre fichier dans une autre repertoire, qui depend sur une fichier dans 
la repertoire originelle:

(~/.coqrc): Add LoadPath rep1 rep2. (*Ou quelque chose comme ca *)
(rep1/top.v): Require Export med.
(rep2/med.v): Require Export bot.
(rep1/bot.v): (* Require Export autre_fichier_se_trouvant_pe_a_rep2. *)

Evidemment, dans ces cas il n'y a pas le possibilite de seulement 
compiler la repertoire rep1 (ou rep2).

Jasper
--
Het verschil tussen theorie en praktijk is dat in theorie
er geen verschil is tussen theorie en praktijk.