diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix
index 0edbc90dfa6c..da6b2f40e62a 100644
--- a/pkgs/applications/science/logic/coq/default.nix
+++ b/pkgs/applications/science/logic/coq/default.nix
@@ -59,6 +59,7 @@ let
    "8.19.1".sha256   = "sha256-kmZ8Uk8jpzjOd67aAPp3C+vU2oNaBw9pr7+Uixcgg94=";
    "8.19.2".sha256   = "sha256-q+i07JsMZp83Gqav6v1jxsgPLN7sPvp5/oszVnavmz0=";
    "8.20.0".sha256   = "sha256-WFpZlA6CzFVAruPhWcHQI7VOBVhrGLdFzWrHW0DTSl0=";
+   "8.20.1".sha256   = "sha256-nRaLODPG4E3gUDzGrCK40vhl4+VhPyd+/fXFK/HC3Ig=";
   };
   releaseRev = v: "V${v}";
   fetched = import ../../../../build-support/coq/meta-fetch/default.nix
diff --git a/pkgs/development/coq-modules/compcert/default.nix b/pkgs/development/coq-modules/compcert/default.nix
index b24a2ea37176..fa694b632a03 100644
--- a/pkgs/development/coq-modules/compcert/default.nix
+++ b/pkgs/development/coq-modules/compcert/default.nix
@@ -278,6 +278,24 @@ let
                 url = "https://github.com/AbsInt/CompCert/commit/20a5b48758bf8ac18e4c420df67017b371efc237.patch";
                 hash = "sha256-TJ87CvLiAv1absGnPsTXsD/HQwKgS82loUTcosulyso=";
               })
+              # Support for Coq 8.20.1
+              (fetchpatch {
+                url = "https://github.com/AbsInt/CompCert/commit/e6c9a2d068ae67923bbc7c6b7035b6afde6ece3c.patch";
+                hash = "sha256-PtiEkG/aLRotIiqrmc6SQncQSi7IGSC5QX3e52xkOUQ=";
+              })
+            ];
+          }
+          {
+            cases = [
+              (isEq "8.20")
+              (isEq "3.15")
+            ];
+            out = [
+              # Support for Coq 8.20.1
+              (fetchpatch {
+                url = "https://github.com/AbsInt/CompCert/commit/e524b0a19ae5140f64047b1cba6ebbe1d16d5bbf.patch";
+                hash = "sha256-24kt0hA75ooyXymH+kNS5VlsuXMHbkqTw4m+BzNUwrw=";
+              })
             ];
           }
         ]