diff --git a/pkgs/development/coq-modules/compcert/default.nix b/pkgs/development/coq-modules/compcert/default.nix
index 28a08f0039f7..a8edc6931a3d 100644
--- a/pkgs/development/coq-modules/compcert/default.nix
+++ b/pkgs/development/coq-modules/compcert/default.nix
@@ -29,7 +29,7 @@ compcert = mkCoqDerivation {
   releaseRev = v: "v${v}";
 
   defaultVersion =  with lib.versions; lib.switch coq.version [
-      { case = range "8.14" "8.19"; out = "3.14"; }
+      { case = range "8.14" "8.20"; out = "3.14"; }
       { case = isEq "8.13"        ; out = "3.10"; }
       { case = isEq "8.12"       ; out = "3.9"; }
       { case = range "8.8" "8.11"; out = "3.8"; }
@@ -201,13 +201,18 @@ patched_compcert = compcert.overrideAttrs (o:
           })
         ];
       }
-      { cases = [ (isEq "8.19") (isEq "3.14") ];
+      { cases = [ (range "8.19" "8.20") (isEq "3.14") ];
         out = [
           # Support for Coq 8.19.2
           (fetchpatch {
             url = "https://github.com/AbsInt/CompCert/commit/8fcfb7d2a6e9ba44003ccab0dfcc894982779af1.patch";
             hash = "sha256-m/kcnDBBPWFriipuGvKZUqLQU8/W1uqw8j4qfCwnTZk=";
           })
+          # Support for Coq 8.20.0
+          (fetchpatch {
+            url = "https://github.com/AbsInt/CompCert/commit/20a5b48758bf8ac18e4c420df67017b371efc237.patch";
+            hash = "sha256-TJ87CvLiAv1absGnPsTXsD/HQwKgS82loUTcosulyso=";
+          })
         ];
       }
     ] [];
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 9afca4a121b2..4077bd7c430c 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -14508,7 +14508,7 @@ with pkgs;
     ocamlPackages = ocaml-ng.ocamlPackages_4_14;
   };
 
-  inherit (coqPackages_8_19) compcert;
+  inherit (coqPackages) compcert;
 
   computecpp-unwrapped = callPackage ../development/compilers/computecpp { };
   computecpp = wrapCCWith rec {