See https://coq.inria.fr/distrib/V8.16.0/refman/changes.html for changes in coq 8.16.0.

Changes in flocq 4.0.0:

• made Coq 8.12 the minimal version and removed the IEEE754.SpecFloatCompat layer
• removed automatic export of ZArith and Reals from Core.Raux and Core.Core
• proved a close/far-path adder in Calc.Plus
• made IEEE754.Binary a wrapper around IEEE754.BinarySingleNaN

Changes in flocq 4.1.0:

• added Bnearbyint and Btrunc in IEEE754
• ensured compatibility from Coq 8.12 to 8.16

Changes in why3 1.5.1:

• Numerous bug fixes
• Documentation
  • documented most options of why3 prove and why3 execute
• Python language
  • added construct e1 if e2 else e3
  • added support for tuples and multiple assignments
  • added #@ axiom and #@ lemma
  • global variables annotated with #@ constant are available in the logic
  • pure functions (i.e., limited to return e) annotated with #@ function are available in the logic
  • logical functions can be given a variant with variant {term}
• Provers
  • support for Z3 4.9.0 and 4.9.1 (released July 6, 2022)
  • support for Z3 4.10.0, 4.10.1 and 4.10.2 (released July 30, 2022)
  • support for Z3 4.11.0 (released August 18, 2022)
  • support for Coq 8.16.0 (release September 5, 2022)
  • support for Gappa 1.4.0 (released April 16, 2022)

The frama-c, gappalib-coq, ocaml-menhir, and zenon builds are simple rebuilds due to the above changes.