Version 1.1 for Rocq 9.0.1

This release updates to Rocq 9.0. Besides this, there are two new contributions, from @dominik-kirst in collaboration with two new contributors:

• @Janis-Bai contributes a mechanisation of Hilbert systems for FO (proven equivalent to ND), and a mechanisation of Gödel's first incompleteness theorem and Tarski's theorem via Carnap's diagonal lemma. (in #8)
• @HaoyiZeng contributes the BDP paper mechanization (in #9)

These improvements are significant enough to bump the version number, making this version 1.1.

Thanks a lot to all involved 🎉

Version 1.0 for Coq 8.20

This release updates to 8.20. The changes are minor, mostly fixing warnings and future-proofing code for the inevitable update to Rocq 9.0.

Initial Release (v1.8+8.18) for Coq 8.18

This release updates the library to Coq 8.18. It includes the Tennenbaum development, and re-licenses the library to MIT.

This version is the first with a version number, namely 1.0.

v1.0+8.17 for Coq 8.17

This release backports the v1.0+8.18 release to Coq 8.17.

Tennenbaum's Theorem

This fixes the state of the FOL library corresponding to the journal version of the paper "An Analysis of Tennenbaum's Theorem in Constructive Type Theory" by Marc Hermes and Dominik Kirst.