diff --git a/pkgs/development/coq-modules/compcert/default.nix b/pkgs/development/coq-modules/compcert/default.nix
index cea8a38b575e..3411863730c6 100644
--- a/pkgs/development/coq-modules/compcert/default.nix
+++ b/pkgs/development/coq-modules/compcert/default.nix
@@ -41,8 +41,8 @@ let
       with lib.versions;
       lib.switch coq.version [
         {
-          case = range "8.15" "9.0";
-          out = "3.16";
+          case = range "8.15" "9.1";
+          out = "3.17";
         }
         {
           case = range "8.14" "8.20";
@@ -73,6 +73,7 @@ let
       "3.14".sha256 = "sha256-QXJMpp/BaPiK5okHeo2rcmXENToXKjB51UqljMHTDgw=";
       "3.15".sha256 = "sha256-QFTueGZd0hAWUj+c5GZL/AyNpfN4FuJiIzCICmwRXJ8=";
       "3.16".sha256 = "sha256-Ep8bcSFs3Cu+lV5qgo89JJU2vh4TTq66Or0c4evo3gM=";
+      "3.17".hash = "sha256-RRc39FUe2sHQdO/ybwA3B7o31qfxcUkgah6I20i0ElE=";
     };
 
     strictDeps = true;
@@ -316,6 +317,19 @@ let
               })
             ];
           }
+          {
+            cases = [
+              (isGe "9.0")
+              (isEq "3.17")
+            ];
+            out = [
+              # Support for Coq 9.0.1 & Coq 9.1.1
+              (fetchpatch {
+                url = "https://github.com/AbsInt/CompCert/commit/6e5d40fb028d787249cd897fe4a1b96420addb8b.patch";
+                hash = "sha256-YBDsvhfup1IMc5GcW7BdsHUKGCv3A1eGIeb4Wal4x7A=";
+              })
+            ];
+          }
         ]
         [ ];
   });