Home My Page Projects Flocq
Summary Activity Tracker News SCM Files

Project Filelist for Flocq

File Release Notes and Changelog

Release Name: 2.5.0

Change Log
Version 2.5.0:
 - ensured compatibility with both Coq 8.4 and 8.5
   (Flocq now provides its own version of iter_pos)
 - redefined ulp, so that ulp(0) is meaningful
 - renamed, generalized, and added lemmas in Fcore_ulp
 - extended predecessor and successor to nonpositive values
   (the previous definition of pred has been renamed pred_pos)
 - removed some hypotheses on lemmas of Fprop_relative
 - added more examples
   . Average: proof on Sterbenz's average and correctly-rounded average
   . Cody_Waite: Cody & Waite's approximation of exponential
   . Compute: effective FP computations with an example of sqrt(sqr(x))
     in radix 5 and precision 3
   . Division_u16: integer division using floating-point FMA
   . Triangle: Kahan's algorithm for the area of a triangle