The Coq mailing list

[Michael<michaelschausten AT googlemail.com>]

Hello,

I wanted to install Gappa to prove floating arithmetics programs in Coq, but i
received an error i couldn't solve.
I first installed the latest gappa release (0.13.0) with (./configure && make
&& make install), which worked fine (after having installed gmp, mpfr and
boost). I then downloaded the "Coq support library 0.13" and ran 
"./configure".
Then i wanted to use "make" to compile the files, which started compiling
various *.v - files with coqdep and coqc.
Then the script ran "OCAMLOPT gappatac.ml" and failed with the following 
error:

OCAMLOPT gappatac.ml
File "gappatac.ml", line 10, characters 0-9:
Error: Unbound module Util
make[1]: *** [gappatac.cmxs] Fehler 2
make[1]: Verlasse Verzeichnis '/home/user/gappalib-coq-0.13/src'
make: *** [all-recursive] Fehler 1

I couldn't figure out where to find that module Util, or what to do to compile
it properly. I hope someone can help me with that problem.

Sincerely,