--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on August 2014 ---
Hello Jerry, > > 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 > You must have flocq 2.3.0. I have it :) > You'll need this patch: > > --- lib/coq/WhyFloats.v.orig 2014-03-17 16:01:46.000000000 -0600 > +++ lib/coq/WhyFloats.v 2014-04-21 15:39:55.680771647 -0600 > @@ -108,7 +108,7 @@ > generalize (Zeq_bool_eq _ _ H1). clear. > rewrite Fcalc_digits.Z_of_nat_S_digits2_Pnat. > intros H. > -apply (Fcalc_digits.Zpower_gt_Zdigits Fcalc_digits.radix2 (Zpos prec) > (Zpos m)). > +apply (Fcore_digits.Zpower_gt_Zdigits Fcalc_digits.radix2 (Zpos prec) > (Zpos m)). > revert H. > unfold FLT_exp. > generalize (Fcore_digits.Zdigits radix2 (Zpos m)). Oh nice, that did the trick. With best regards Christoph