The Coq mailing list

[Michael<michaelschausten AT googlemail.com>]

Gappa installation now worked with libcoq-ocaml-dev installed.

Since I got the coq proof obligations from frama-c jessie plugin via C code,
with the new floating point operations I now have a couple of references coq
doesn't find.

The reference "double_value x" wasn't found at first, I could solve this
problem by manually downloading the floating point library from the coq
website, compliling *.v and copying it to /usr/lib/coq/user-contrib/. Then I
could "Require Export Float." (which wasn't possible before).
However, there's still a couple of references coq doesn't find
(no_overflow_double, nearest_even, double_of_real_post, truncate_real_to_int).
How can I find out which modules I have to load, and where to find them?

Sincerely,