# 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