--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on August 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] why-2.34 compile problem



Hello list,

> now I'm trying to get why-2.34 compiled but I ran into trouble:

Another problem:
WHYLIB=lib bin/why.opt --no-pervasives -tc lib/why/prelude.why
for f in lib/why/bool.why lib/why/integer.why lib/why/divisions.why lib/why/real.why lib/why/arrays.why lib/why/jessie.why lib/why/jessie_bitvectors.why lib/why/mybag.why lib/why/mix.why lib/why/floats_common.why lib/why/floats_strict.why lib/why/floats_full.why lib/why/floats_multi_rounding.why  ; do \
                WHYLIB=lib bin/why.opt -tc $f; \
        done
coqc  -R lib/coq Why lib/coq/WhyFloats.v
File "/home/crissi/frama-c/why-2.34/lib/coq/WhyFloats.v", line 111, characters 7-37:
Error: The reference Fcalc_digits.Zpower_gt_Zdigits was not found
in the current environment.
make: *** [lib/coq/WhyFloats.vo] Error 1


Any ideas?

With best regards

Christoph