The Coq mailing list

[Houda Anoun <anoun AT labri.fr>]

Bonjour tt le monde,
Je suis en train de réaliser un développement qui comprend plusieurs 
répertoires contenant différents fichiers Coq...
Je voulais savoir comment résoudre le probleme qui se pose à cause de la 
dependance entre des fichiers Coq se trouvant ds des repertoires 
differents...dans ce cas, la commande Require rep/fichier ne marche pas ?!
Une solution pas tres elegante est d'inclure la commande 'Add LoadPath 
rep' au début de chaque fichier qui utilise des fichiers se trouvant ds 
'rep'...
Je me demande s'il y'a pas une autre solution plus élégante?!
Le second probleme, est celui de la compilation, en effet, pour chaque 
repertoire il y'a un makefile qui permet de compiler ses fichiers .... 
bien evidemment il y'aura un certain ordre qu'il faut respecter lors de 
la compilation 'compiler les fichiers de rep1 avant ceux de rep2 etc...'...
je veux savoir s'il y'a pas un outil génerique qui permet de compiler 
tous les fichiers se trouvant ds des repertoires differents?
Je vous remercie
Cordialement
Houda