--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on August 2014 ---
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