The Coq mailing list

[Michael<michaelschausten AT googlemail.com>]

Hello,

I downloaded Floats8.2.tgz from https://lipforge.ens-lyon.fr/projects/pff/ and
tried to compile and install ist.
I first try to use the Makefile included in the archive, with "make depend &&
make all && sudo make install", however it did not find some dependencies.
I then tried to create the Makefile on my own, with "coq_makefile *.v >
Makefile". However, it already gives a warning:
"Warning: install target will copy files at the first level of the coq
contributions installation directory; option -R is recommended"
I think it is because of the subdirectories in the Float8.2 package. If I
ignore the warning, make simply puts all *.vo files in the
/usr/lib/coq/user-contrib/Float/, but withouth any subdirectories. The result
is, that a lot of libraries can't be found by other proof skripts later (even
moving them to the right subdirectories manually later on does not help).

Can somebody help me, how to get the installation correctly done? Maybe it's
just because of the option "-R" recommended in the warning, but I don't know
how to apply it on all subdirectories.


Sincerely,