This release has been tested for compatibility with Coq 8.13-8.15 and MathComp 1.12-1.14. The gaia-hydras package requires Coq 8.14 or later.
Release highlights
The experimental bridge to the Gaia project allows now to import some definitions and theorems of the so-called Ketonen-Solovay combinatorial machinery into the Gaia environment (see Chapter 7 of the documentation).
The first topics treated in this version are: canonical sequences, accessibility, and a few rapidly growing hierarchies of arithmetical functions.
Revision book to page 82. deprecate a few symbols by @Casteran in #130
Full Changelog: v0.6...v0.9
Contributors
Casteran