Merge PR #7950: Documentation for 8.8.1

2 files changed, 12 insertions, 1 deletions

diff --git a/CHANGES b/CHANGES
index 44186d30c..75f4df06a 100644
--- a/CHANGES
+++ b/CHANGES
@@ -91,6 +91,7 @@ Changes from 8.8.0 to 8.8.1
 Kernel
 
 - Fix a critical bug with cofixpoints and vm_compute/native_compute (#7333).
+- Fix a critical bug with modules and algebraic universes (#7695)
 - Fix a critical bug with inlining of polymorphic constants (#7615).
 - Fix a critical bug with universe polymorphism and vm_compute (#7723). Was
   present since 8.5.
@@ -100,6 +101,16 @@ Notations
 - Fixed unexpected collision between only-parsing and only-printing
   notations (issue #7462).
 
+Windows installer
+
+- The Windows installer now includes external packages Ltac2 and Equations
+  (it included the Bignums package since 8.8+beta1).
+
+Many other bug fixes, documentation improvements (including fixes of
+regressions due to the Sphinx migration), and user message improvements
+(for details, see the 8.8.1 milestone at
+https://github.com/coq/coq/milestone/13?closed=1).
+
 Changes from 8.8+beta1 to 8.8.0
 ===============================
 
diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits.rst
index 2562dec46..5d9324a65 100644
--- a/doc/sphinx/credits.rst
+++ b/doc/sphinx/credits.rst
@@ -1393,7 +1393,7 @@ Version 8.8 is the third release of |Coq| developed on a time-based
 development cycle. Its development spanned 6 months from the release of
 |Coq| 8.7 and was based on a public roadmap. The development process
 was coordinated by Matthieu Sozeau. Maxime Dénès was in charge of the
-release process.
+release process. Théo Zimmermann is the maintainer of this release.
 
 Many power users helped to improve the design of the new features via
 the bug tracker, the pull request system, the |Coq| development mailing