diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 3d0e4edae..ef1edc75d 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -129,26 +129,20 @@ jobs:
           - coq-8.18.0-emacs-26.3
           - coq-8.18.0-emacs-27.1
           - coq-8.18.0-emacs-28.2
-          - coq-8.18.0-emacs-29.1
           - coq-8.18.0-emacs-29.4
           - coq-8.19.2-emacs-26.3
           - coq-8.19.2-emacs-27.1
-          - coq-8.19.2-emacs-27.2
-          - coq-8.19.2-emacs-28.1
           - coq-8.19.2-emacs-28.2
-          - coq-8.19.2-emacs-29.1
-          - coq-8.19.2-emacs-29.2
-          - coq-8.19.2-emacs-29.3
           - coq-8.19.2-emacs-29.4
-          - coq-8.20-rc1-emacs-26.3
-          - coq-8.20-rc1-emacs-27.1
-          - coq-8.20-rc1-emacs-27.2
-          - coq-8.20-rc1-emacs-28.1
-          - coq-8.20-rc1-emacs-28.2
-          - coq-8.20-rc1-emacs-29.1
-          - coq-8.20-rc1-emacs-29.2
-          - coq-8.20-rc1-emacs-29.3
-          - coq-8.20-rc1-emacs-29.4
+          - coq-8.20.0-emacs-26.3
+          - coq-8.20.0-emacs-27.1
+          - coq-8.20.0-emacs-27.2
+          - coq-8.20.0-emacs-28.1
+          - coq-8.20.0-emacs-28.2
+          - coq-8.20.0-emacs-29.1
+          - coq-8.20.0-emacs-29.2
+          - coq-8.20.0-emacs-29.3
+          - coq-8.20.0-emacs-29.4
           # CIPG change marker end
       # don't cancel all in-progress jobs if one matrix job fails:
       fail-fast: false
@@ -211,26 +205,20 @@ jobs:
           - coq-8.18.0-emacs-26.3
           - coq-8.18.0-emacs-27.1
           - coq-8.18.0-emacs-28.2
-          - coq-8.18.0-emacs-29.1
           - coq-8.18.0-emacs-29.4
           - coq-8.19.2-emacs-26.3
           - coq-8.19.2-emacs-27.1
-          - coq-8.19.2-emacs-27.2
-          - coq-8.19.2-emacs-28.1
           - coq-8.19.2-emacs-28.2
-          - coq-8.19.2-emacs-29.1
-          - coq-8.19.2-emacs-29.2
-          - coq-8.19.2-emacs-29.3
           - coq-8.19.2-emacs-29.4
-          - coq-8.20-rc1-emacs-26.3
-          - coq-8.20-rc1-emacs-27.1
-          - coq-8.20-rc1-emacs-27.2
-          - coq-8.20-rc1-emacs-28.1
-          - coq-8.20-rc1-emacs-28.2
-          - coq-8.20-rc1-emacs-29.1
-          - coq-8.20-rc1-emacs-29.2
-          - coq-8.20-rc1-emacs-29.3
-          - coq-8.20-rc1-emacs-29.4
+          - coq-8.20.0-emacs-26.3
+          - coq-8.20.0-emacs-27.1
+          - coq-8.20.0-emacs-27.2
+          - coq-8.20.0-emacs-28.1
+          - coq-8.20.0-emacs-28.2
+          - coq-8.20.0-emacs-29.1
+          - coq-8.20.0-emacs-29.2
+          - coq-8.20.0-emacs-29.3
+          - coq-8.20.0-emacs-29.4
           # CIPG change marker end
       # don't cancel all in-progress jobs if one matrix job fails:
       fail-fast: false
@@ -289,26 +277,20 @@ jobs:
           - coq-8.18.0-emacs-26.3
           - coq-8.18.0-emacs-27.1
           - coq-8.18.0-emacs-28.2
-          - coq-8.18.0-emacs-29.1
           - coq-8.18.0-emacs-29.4
           - coq-8.19.2-emacs-26.3
           - coq-8.19.2-emacs-27.1
-          - coq-8.19.2-emacs-27.2
-          - coq-8.19.2-emacs-28.1
           - coq-8.19.2-emacs-28.2
-          - coq-8.19.2-emacs-29.1
-          - coq-8.19.2-emacs-29.2
-          - coq-8.19.2-emacs-29.3
           - coq-8.19.2-emacs-29.4
-          - coq-8.20-rc1-emacs-26.3
-          - coq-8.20-rc1-emacs-27.1
-          - coq-8.20-rc1-emacs-27.2
-          - coq-8.20-rc1-emacs-28.1
-          - coq-8.20-rc1-emacs-28.2
-          - coq-8.20-rc1-emacs-29.1
-          - coq-8.20-rc1-emacs-29.2
-          - coq-8.20-rc1-emacs-29.3
-          - coq-8.20-rc1-emacs-29.4
+          - coq-8.20.0-emacs-26.3
+          - coq-8.20.0-emacs-27.1
+          - coq-8.20.0-emacs-27.2
+          - coq-8.20.0-emacs-28.1
+          - coq-8.20.0-emacs-28.2
+          - coq-8.20.0-emacs-29.1
+          - coq-8.20.0-emacs-29.2
+          - coq-8.20.0-emacs-29.3
+          - coq-8.20.0-emacs-29.4
           # CIPG change marker end
       # don't cancel all in-progress jobs if one matrix job fails:
       fail-fast: false
diff --git a/ci/doc/README.md b/ci/doc/README.md
index eaa6c000d..a59e5803a 100644
--- a/ci/doc/README.md
+++ b/ci/doc/README.md
@@ -168,7 +168,7 @@ This results in
 <!-- The content between the CIPG markers is automatically changed by
  !-- the cipg program. Do not change these markers. -->
 <!-- CIPG change marker: container-number -->
-65
+63
 <!-- CIPG change marker end -->
 containers.
 
@@ -181,15 +181,15 @@ containers.
 |   8.9.1 |      |   H  |      |      |      |      |      |      |      |      |      |
 |  8.10.2 |      |      |   H  |      |      |      |      |      |      |      |      |
 |  8.11.2 |      |      |  SUP |      |      |      |      |      |      |      |   N  |
-|  8.12.2 |      |      |  SUP |  SUP |      |      |      |      |      |      |   N  |
-|  8.13.2 |      |      |  SUP |  SUP |   H  |      |      |      |      |      |   N  |
-|  8.14.1 |      |      |  SUP |  SUP |   H  |      |      |      |      |      |   N  |
+|  8.12.2 |      |      |  SUP |   H  |      |      |      |      |      |      |   N  |
+|  8.13.2 |      |      |  SUP |      |   H  |      |      |      |      |      |   N  |
+|  8.14.1 |      |      |  SUP |      |   H  |      |      |      |      |      |   N  |
 |  8.15.2 |      |      |  SUP |  SUP |      |   H  |      |      |      |      |   N  |
 |  8.16.1 |      |      |   X  |   X  |   X  |   X  |   X  |   X  |   X  |   X  |   X  |
 |  8.17.1 |      |      |   X  |   X  |   X  |   X  |   X  |   X  |   X  |   X  |   X  |
 |  8.18.0 |      |      |   X  |   X  |   X  |   X  |   X  |   X  |   X  |   X  |   X  |
 |  8.19.2 |      |      |   X  |   X  |   X  |   X  |   X  |   X  |   X  |   X  |   X  |
-|  8.20rc |      |      |   RC |   RC |   RC |   RC |   RC |   RC |   RC |   RC |   RC |
+|  8.20.0 |      |      |   X  |   X  |   X  |   X  |   X  |   X  |   X  |   X  |   X  |
 <!-- CIPG change marker end -->
 
 In the table above,
@@ -286,7 +286,7 @@ This results in
 <!-- The content between the CIPG markers is automatically changed by
  !-- the cipg program. Do not change these markers. -->
 <!-- CIPG change marker: testrun-number -->
-41
+35
 <!-- CIPG change marker end -->
 version pairs for the Proof General interaction tests with Coq.
 
@@ -299,15 +299,15 @@ version pairs for the Proof General interaction tests with Coq.
 |   8.9.1 |      |      |      |      |      |      |      |      |      |      |      |
 |  8.10.2 |      |      |      |      |      |      |      |      |      |      |      |
 |  8.11.2 |      |      |  SUP |      |      |      |      |      |      |      |   N  |
-|  8.12.2 |      |      |      |  SUP |      |      |      |      |      |      |   N  |
+|  8.12.2 |      |      |      |   H  |      |      |      |      |      |      |   N  |
 |  8.13.2 |      |      |      |      |   H  |      |      |      |      |      |   N  |
 |  8.14.1 |      |      |      |      |   H  |      |      |      |      |      |   N  |
 |  8.15.2 |      |      |      |  SUP |      |   H  |      |      |      |      |   N  |
 |  8.16.1 |      |      |      |      |      |      |  SUP |      |      |      |   N  |
-|  8.17.1 |      |      |   X  |   X  |      |      |   X  |   X  |      |      |   N  |
-|  8.18.0 |      |      |   X  |   X  |      |      |   X  |   X  |      |      |   N  |
-|  8.19.2 |      |      |   X  |   X  |   N  |   N  |   X  |   X  |   N  |   N  |   N  |
-|  8.20rc |      |      |   RC |   RC |   RC |   RC |   RC |   RC |   RC |   RC |   RC |
+|  8.17.1 |      |      |   X  |   X  |      |      |   X  |   H  |      |      |   N  |
+|  8.18.0 |      |      |   X  |   X  |      |      |   X  |      |      |      |   N  |
+|  8.19.2 |      |      |   X  |   X  |      |      |   X  |      |      |      |   N  |
+|  8.20.0 |      |      |   X  |   X  |   N  |   N  |   X  |   N  |   N  |   N  |   N  |
 <!-- CIPG change marker end -->
 
 See [Container build strategy](#contbuild) for an explanation of the
@@ -317,7 +317,7 @@ In summary, all Proof General testing jobs run
 <!-- The content between the CIPG markers is automatically changed by
  !-- the cipg program. Do not change these markers. -->
 <!-- CIPG change marker: total-checks-number -->
-152
+134
 <!-- CIPG change marker end -->
 github checks.
 
diff --git a/ci/doc/coq-emacs-releases.org b/ci/doc/coq-emacs-releases.org
index e313bb8b2..ad22dee64 100644
--- a/ci/doc/coq-emacs-releases.org
+++ b/ci/doc/coq-emacs-releases.org
@@ -13,7 +13,7 @@
 
 | date    |    coq | emacs | distribution name | EOL      | historic |
 |---------+--------+-------+-------------------+----------+----------|
-| 2024/06 | 8.20rc |       |                   |          |          |
+| 2024/09 | 8.20.0 |       |                   |          |          |
 | 2024/06 | 8.19.2 |  29.4 |                   |          |          |
 | 2024/03 | 8.19.1 |  29.3 |                   |          |          |
 | 2024/01 | 8.19.0 |  29.2 |                   |          |          |
@@ -40,7 +40,7 @@
 | 2020/12 | 8.12.2 |       |                   |          | X        |
 | 2020/11 | 8.12.1 |       |                   |          |          |
 | 2021/10 |        |       | ubu 21 impish     | 2022/07  |          |
-| 2021/08 |        |       | deb 11 bullseye   | 2024/07? |          |
+| 2021/08 |        |       | deb 11 bullseye   | 2024/08  |          |
 | 2020/08 |        |  27.1 |                   |          |          |
 | 2020/07 | 8.12.0 |       |                   |          |          |
 | 2020/06 | 8.11.2 |       |                   |          |          |
diff --git a/ci/doc/currently-used-coq-emacs-versions b/ci/doc/currently-used-coq-emacs-versions
index 96a336895..e681d2581 100644
--- a/ci/doc/currently-used-coq-emacs-versions
+++ b/ci/doc/currently-used-coq-emacs-versions
@@ -7,11 +7,9 @@ coq-8.12.2-emacs-26.3
 coq-8.12.2-emacs-27.1
 coq-8.12.2-emacs-29.4
 coq-8.13.2-emacs-26.3
-coq-8.13.2-emacs-27.1
 coq-8.13.2-emacs-27.2
 coq-8.13.2-emacs-29.4
 coq-8.14.1-emacs-26.3
-coq-8.14.1-emacs-27.1
 coq-8.14.1-emacs-27.2
 coq-8.14.1-emacs-29.4
 coq-8.15.2-emacs-26.3
@@ -54,12 +52,12 @@ coq-8.19.2-emacs-29.1
 coq-8.19.2-emacs-29.2
 coq-8.19.2-emacs-29.3
 coq-8.19.2-emacs-29.4
-coq-8.20-rc1-emacs-26.3
-coq-8.20-rc1-emacs-27.1
-coq-8.20-rc1-emacs-27.2
-coq-8.20-rc1-emacs-28.1
-coq-8.20-rc1-emacs-28.2
-coq-8.20-rc1-emacs-29.1
-coq-8.20-rc1-emacs-29.2
-coq-8.20-rc1-emacs-29.3
-coq-8.20-rc1-emacs-29.4
+coq-8.20.0-emacs-26.3
+coq-8.20.0-emacs-27.1
+coq-8.20.0-emacs-27.2
+coq-8.20.0-emacs-28.1
+coq-8.20.0-emacs-28.2
+coq-8.20.0-emacs-29.1
+coq-8.20.0-emacs-29.2
+coq-8.20.0-emacs-29.3
+coq-8.20.0-emacs-29.4
diff --git a/ci/doc/currently-used-coq-nix-versions b/ci/doc/currently-used-coq-nix-versions
index 125c320e9..ccb4dff58 100644
--- a/ci/doc/currently-used-coq-nix-versions
+++ b/ci/doc/currently-used-coq-nix-versions
@@ -10,4 +10,4 @@
 8.17.1
 8.18.0
 8.19.2
-8.20rc
+8.20.0