Hi, Jiří Paleček wrote: > I tried to check some simple program usign floats and discovered it > was impossible with why. The reason is that the file WhyFloats.v is > missing, which is caused by the float library missing during the > build. I think it should be possible to check programs with floats, > which could be accomplished by three ways: > > Take the float library from http://coq.inria.fr/contribs/Float.tar.gz > and either > > - add it to the coq-libs package, and make why build-dep on coq-libs > - make an extra package coq-lib-float, and -"- > - add this library to the why package itself > > What do you think?
First, sorry for taking so long for answering. I think that I'll go for a new package (coq-lib-float) and make why depend on it (or at least recommend it). Thanks for your feedback on this package. Cheers, Samuel.
