The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>]

Hi,
I do not understand what you want.

Is it
I've got A.v, foo/B.v, foo/C.v where A Requires Foo.B and B Requires  
Foo.C.
I write

-R . toto
A.v

in my _CoqProject file. I do coq_makefile -f _CoqProject -o Makefile
and I expect everything to work ?

This will not because of dependencies; only the one of listed files  
are compute so you will have
A.vo: foo/B.vo
but nothing that say
foo/B.vo: foo/C.vo
and C will no be compiled.

I may complitely miss the point and, because I need to rewrite  
coq_makefile documentation, I'm interressted to get more information.

All the best,
Pierre Boutillier

Le 22 févr. 12 à 04:22, Gyesik Lee a écrit :

> Hi,
>
> would someone remind me of how to create Makefile such that all the  
> dependent files in subdirectories or special directories can be  
> automatically involved during compilation?
>
> I tried to follow the instructions from the coq_makefile --help, but  
> failed.
>
> Any help would be appreciated.
>
> Gyesik