flocq-2.5.0-1.fc23

• 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

gappalib-coq-1.2.0-1.fc23

• fact database
  • improved handling of powers of two in mul_flt
  • fixed incorrect computation of the order-3 term of the relative error for division
  • added rewriting rules for emulating reverse propagation
• proof graph
  • improved proof simplification
• proof paths
  • improved performances by avoiding some absolute values
  • improved detection of approximate/exact pairs of expressions

why3-0.86.2-1.fc23

• Minor bugfix release
• Compatibility with flocq 2.5.0
• Do not ship the nonfree boomy icons

why-2.35-9.fc23

• Rebuild for flocq 2.5.0, gappalib-coq 1.2.0, and why3 0.86.2