diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix
index da6b2f40e62a..848a69a3f2cc 100644
--- a/pkgs/applications/science/logic/coq/default.nix
+++ b/pkgs/applications/science/logic/coq/default.nix
@@ -60,6 +60,7 @@ let
    "8.19.2".sha256   = "sha256-q+i07JsMZp83Gqav6v1jxsgPLN7sPvp5/oszVnavmz0=";
    "8.20.0".sha256   = "sha256-WFpZlA6CzFVAruPhWcHQI7VOBVhrGLdFzWrHW0DTSl0=";
    "8.20.1".sha256   = "sha256-nRaLODPG4E3gUDzGrCK40vhl4+VhPyd+/fXFK/HC3Ig=";
+   "9.0+rc1".sha256  = "sha256-TLq925HFdizxyHjKRMeHBH9rLRpLNUiVIfA1JSMgYXA=";
   };
   releaseRev = v: "V${v}";
   fetched = import ../../../../build-support/coq/meta-fetch/default.nix
diff --git a/pkgs/development/coq-modules/Cheerios/default.nix b/pkgs/development/coq-modules/Cheerios/default.nix
index 8bdcbab8370a..92a1525463b6 100644
--- a/pkgs/development/coq-modules/Cheerios/default.nix
+++ b/pkgs/development/coq-modules/Cheerios/default.nix
@@ -14,7 +14,7 @@ mkCoqDerivation {
     with lib.versions;
     lib.switch coq.version [
       {
-        case = range "8.14" "8.20";
+        case = range "8.14" "9.0";
         out = "20230107";
       }
       {
diff --git a/pkgs/development/coq-modules/CoLoR/default.nix b/pkgs/development/coq-modules/CoLoR/default.nix
index 3677f65625bb..7fadc2f74649 100644
--- a/pkgs/development/coq-modules/CoLoR/default.nix
+++ b/pkgs/development/coq-modules/CoLoR/default.nix
@@ -14,7 +14,7 @@ mkCoqDerivation {
     with lib.versions;
     lib.switch coq.version [
       {
-        case = range "8.14" "8.20";
+        case = range "8.14" "9.0";
         out = "1.8.5";
       }
       {
diff --git a/pkgs/development/coq-modules/ElmExtraction/default.nix b/pkgs/development/coq-modules/ElmExtraction/default.nix
index 0a7a22c812a2..cfba9df2a660 100644
--- a/pkgs/development/coq-modules/ElmExtraction/default.nix
+++ b/pkgs/development/coq-modules/ElmExtraction/default.nix
@@ -25,7 +25,7 @@ mkCoqDerivation {
       [
         {
           cases = [
-            (range "8.17" "8.20")
+            (range "8.17" "9.0")
             (range "1.3.1" "1.3.2")
           ];
           out = "0.1.0";
diff --git a/pkgs/development/coq-modules/ExtLib/default.nix b/pkgs/development/coq-modules/ExtLib/default.nix
index 4eb989a50ef4..90fd3a261639 100644
--- a/pkgs/development/coq-modules/ExtLib/default.nix
+++ b/pkgs/development/coq-modules/ExtLib/default.nix
@@ -4,7 +4,7 @@ mkCoqDerivation rec {
   pname = "coq-ext-lib";
   inherit version;
   defaultVersion = with lib.versions; lib.switch coq.coq-version [
-    { case = range "8.14" "8.20"; out = "0.13.0"; }
+    { case = range "8.14" "9.0"; out = "0.13.0"; }
     { case = range "8.11" "8.19"; out = "0.12.0"; }
     { case = range "8.8" "8.16"; out = "0.11.6"; }
     { case = range "8.8" "8.14"; out = "0.11.4"; }
diff --git a/pkgs/development/coq-modules/ITree/default.nix b/pkgs/development/coq-modules/ITree/default.nix
index 218d7e2f3be8..981afa1180bd 100644
--- a/pkgs/development/coq-modules/ITree/default.nix
+++ b/pkgs/development/coq-modules/ITree/default.nix
@@ -14,7 +14,7 @@ mkCoqDerivation rec {
   defaultVersion =
     with lib.versions;
     lib.switch coq.version [
-      { case = range "8.13" "8.20"; out = "5.2.0+20241009"; }
+      { case = range "8.13" "9.0"; out = "5.2.0+20241009"; }
       { case = range "8.10" "8.16"; out = "4.0.0"; }
     ] null;
   release."5.2.0+20241009".sha256 = "sha256-eg47YgnIonCq7XOUgh9uzoKsuFCvsOSTZhgFLNNcPD0=";
diff --git a/pkgs/development/coq-modules/InfSeqExt/default.nix b/pkgs/development/coq-modules/InfSeqExt/default.nix
index 479205b0245a..42b6aa0b6f42 100644
--- a/pkgs/development/coq-modules/InfSeqExt/default.nix
+++ b/pkgs/development/coq-modules/InfSeqExt/default.nix
@@ -14,7 +14,7 @@ mkCoqDerivation {
     with lib.versions;
     lib.switch coq.version [
       {
-        case = range "8.9" "8.20";
+        case = range "8.9" "9.0";
         out = "20230107";
       }
       {
diff --git a/pkgs/development/coq-modules/MenhirLib/default.nix b/pkgs/development/coq-modules/MenhirLib/default.nix
index f2c5a217c8ff..4e3f0ec0b4cb 100644
--- a/pkgs/development/coq-modules/MenhirLib/default.nix
+++ b/pkgs/development/coq-modules/MenhirLib/default.nix
@@ -16,7 +16,7 @@ let
       with lib.versions;
       lib.switch coq.coq-version [
         {
-          case = range "8.12" "8.20";
+          case = range "8.12" "9.0";
           out = "20240715";
         }
         {
diff --git a/pkgs/development/coq-modules/QuickChick/default.nix b/pkgs/development/coq-modules/QuickChick/default.nix
index 0f70982dfaf1..a18acb3120e3 100644
--- a/pkgs/development/coq-modules/QuickChick/default.nix
+++ b/pkgs/development/coq-modules/QuickChick/default.nix
@@ -21,7 +21,7 @@ in
       [
         {
           cases = [
-            (lib.versions.range "8.15" "8.20")
+            (lib.versions.range "8.15" "9.0")
             lib.pred.true
           ];
           out = "2.0.4";
diff --git a/pkgs/development/coq-modules/StructTact/default.nix b/pkgs/development/coq-modules/StructTact/default.nix
index 63a450726e4c..594eb183b7b0 100644
--- a/pkgs/development/coq-modules/StructTact/default.nix
+++ b/pkgs/development/coq-modules/StructTact/default.nix
@@ -14,7 +14,7 @@ mkCoqDerivation {
     with lib.versions;
     lib.switch coq.coq-version [
       {
-        case = range "8.9" "8.20";
+        case = range "8.9" "9.0";
         out = "20230107";
       }
       {
diff --git a/pkgs/development/coq-modules/autosubst/default.nix b/pkgs/development/coq-modules/autosubst/default.nix
index e5fd36cd7f05..ce28e4a0d911 100644
--- a/pkgs/development/coq-modules/autosubst/default.nix
+++ b/pkgs/development/coq-modules/autosubst/default.nix
@@ -20,7 +20,7 @@ mkCoqDerivation {
     with lib.versions;
     lib.switch coq.coq-version [
       {
-        case = range "8.14" "8.20";
+        case = range "8.14" "9.0";
         out = "1.9";
       }
       {
diff --git a/pkgs/development/coq-modules/bignums/default.nix b/pkgs/development/coq-modules/bignums/default.nix
index acd6b8e04303..9dd77a802105 100644
--- a/pkgs/development/coq-modules/bignums/default.nix
+++ b/pkgs/development/coq-modules/bignums/default.nix
@@ -13,6 +13,10 @@ mkCoqDerivation {
   defaultVersion =
     with lib.versions;
     lib.switch coq.coq-version [
+      {
+        case = range "9.0" "9.0";
+        out = "9.0.0+rocq${coq.coq-version}";
+      }
       {
         case = range "8.13" "8.20";
         out = "9.0.0+coq${coq.coq-version}";
@@ -23,6 +27,7 @@ mkCoqDerivation {
       }
     ] null;
 
+  release."9.0.0+rocq9.0".sha256 = "sha256-ctnwpyNVhryEUA5YEsAImrcJsNMhtBgDSOz+z5Z4R78=";
   release."9.0.0+coq8.20".sha256 = "sha256-pkvyDaMXRalc6Uu1eBTuiqTpRauRrzu946c6TavyTKY=";
   release."9.0.0+coq8.19".sha256 = "sha256-02uL+qWbUveHe67zKfc8w3U0iN3X2DKBsvP3pKpW8KQ=";
   release."9.0.0+coq8.18".sha256 = "sha256-vLeJ0GNKl4M84Uj2tAwlrxJOSR6VZoJQvdlDhxJRge8=";
diff --git a/pkgs/development/coq-modules/ceres/default.nix b/pkgs/development/coq-modules/ceres/default.nix
index b141d2b48e2a..3bf17cb6cf4d 100644
--- a/pkgs/development/coq-modules/ceres/default.nix
+++ b/pkgs/development/coq-modules/ceres/default.nix
@@ -17,7 +17,7 @@ mkCoqDerivation {
     with lib.versions;
     lib.switch coq.version [
       {
-        case = range "8.14" "8.20";
+        case = range "8.14" "9.0";
         out = "0.4.1";
       }
       {
diff --git a/pkgs/development/coq-modules/coq-elpi/default.nix b/pkgs/development/coq-modules/coq-elpi/default.nix
index 18e83c48b1a4..927f9d282131 100644
--- a/pkgs/development/coq-modules/coq-elpi/default.nix
+++ b/pkgs/development/coq-modules/coq-elpi/default.nix
@@ -21,6 +21,7 @@ default-elpi-version = if elpi-version != null then elpi-version else (
     { case = "8.18"; out = "1.18.1"; }
     { case = "8.19"; out = "1.18.1"; }
     { case = "8.20"; out = "1.19.2"; }
+    { case = "9.0"; out = "2.0.7"; }
   ] { }
 );
 elpi = coq.ocamlPackages.elpi.override { version = default-elpi-version; };
@@ -34,6 +35,7 @@ derivation = mkCoqDerivation {
   owner = "LPCIC";
   inherit version;
   defaultVersion = lib.switch coq.coq-version [
+    { case = "9.0"; out = "2.4.0"; }
     { case = "8.20"; out = "2.2.0"; }
     { case = "8.19"; out = "2.0.1"; }
     { case = "8.18"; out = "2.0.0"; }
@@ -45,6 +47,7 @@ derivation = mkCoqDerivation {
     { case = "8.12"; out = "1.8.3_8.12"; }
     { case = "8.11"; out = "1.6.3_8.11"; }
   ] null;
+  release."2.4.0".sha256 = "sha256-W2+vVGExLLux8e0nSZESSoMVvrLxhL6dmXkb+JuKiqc=";
   release."2.2.0".sha256 = "sha256-rADEoqTXM7/TyYkUKsmCFfj6fjpWdnZEOK++5oLfC/I=";
   release."2.0.1".sha256 = "sha256-cuoPsEJ+JRLVc9Golt2rJj4P7lKltTrrmQijjoViooc=";
   release."2.0.0".sha256 = "sha256-A/cH324M21k3SZ7+YWXtaYEbu6dZQq3K0cb1RMKjbsM=";
diff --git a/pkgs/development/coq-modules/coq-record-update/default.nix b/pkgs/development/coq-modules/coq-record-update/default.nix
index ff71c5ecdc43..d4c901ef044f 100644
--- a/pkgs/development/coq-modules/coq-record-update/default.nix
+++ b/pkgs/development/coq-modules/coq-record-update/default.nix
@@ -13,7 +13,7 @@ mkCoqDerivation rec {
     with lib.versions;
     lib.switch coq.coq-version [
       {
-        case = range "8.10" "8.20";
+        case = range "8.10" "9.0";
         out = "0.3.4";
       }
     ] null;
diff --git a/pkgs/development/coq-modules/coqide/default.nix b/pkgs/development/coq-modules/coqide/default.nix
index 8ae04078b771..8bab88333e40 100644
--- a/pkgs/development/coq-modules/coqide/default.nix
+++ b/pkgs/development/coq-modules/coqide/default.nix
@@ -17,7 +17,7 @@ mkCoqDerivation rec {
   inherit (coq) src;
   release."${coq.version}" = { };
 
-  defaultVersion = if lib.versions.isGe "8.14" coq.version then coq.version else null;
+  defaultVersion = if lib.versions.range "8.14" "8.20" coq.version then coq.version else null;
 
   preConfigure = ''
     patchShebangs dev/tools/
diff --git a/pkgs/development/coq-modules/deriving/default.nix b/pkgs/development/coq-modules/deriving/default.nix
index 909cb7f42154..259cf724c316 100644
--- a/pkgs/development/coq-modules/deriving/default.nix
+++ b/pkgs/development/coq-modules/deriving/default.nix
@@ -18,7 +18,7 @@ mkCoqDerivation {
       [
         {
           cases = [
-            (range "8.17" "8.20")
+            (range "8.17" "9.0")
             (isGe "2.0.0")
           ];
           out = "0.2.1";
diff --git a/pkgs/development/coq-modules/extructures/default.nix b/pkgs/development/coq-modules/extructures/default.nix
index 2f5b3f330089..2b5f43f31698 100644
--- a/pkgs/development/coq-modules/extructures/default.nix
+++ b/pkgs/development/coq-modules/extructures/default.nix
@@ -19,7 +19,7 @@
       [
         {
           cases = [
-            (range "8.17" "8.20")
+            (range "8.17" "9.0")
             (isGe "2.0.0")
           ];
           out = "0.5.0";
diff --git a/pkgs/development/coq-modules/gaia/default.nix b/pkgs/development/coq-modules/gaia/default.nix
index 2e17861ea3bf..05079005b6c0 100644
--- a/pkgs/development/coq-modules/gaia/default.nix
+++ b/pkgs/development/coq-modules/gaia/default.nix
@@ -26,7 +26,7 @@ mkCoqDerivation {
       [
         {
           cases = [
-            (range "8.16" "8.20")
+            (range "8.16" "9.0")
             (range "2.0" "2.3")
           ];
           out = "2.2";
diff --git a/pkgs/development/coq-modules/hierarchy-builder/default.nix b/pkgs/development/coq-modules/hierarchy-builder/default.nix
index bff7825637c7..270c9a26d337 100644
--- a/pkgs/development/coq-modules/hierarchy-builder/default.nix
+++ b/pkgs/development/coq-modules/hierarchy-builder/default.nix
@@ -5,6 +5,7 @@ let hb = mkCoqDerivation {
   owner = "math-comp";
   inherit version;
   defaultVersion = with lib.versions; lib.switch coq.coq-version [
+    { case = range "9.0" "9.0";   out = "1.8.1"; }
     { case = range "8.19" "8.20"; out = "1.8.0"; }
     { case = range "8.18" "8.20"; out = "1.7.1"; }
     { case = range "8.16" "8.18"; out = "1.6.0"; }
@@ -14,6 +15,7 @@ let hb = mkCoqDerivation {
     { case = range "8.12" "8.13"; out = "1.1.0"; }
     { case = isEq "8.11";         out = "0.10.0"; }
   ] null;
+  release."1.8.1".sha256  = "sha256-Z0WAHDyycqgL+Le/zNfEAoLWzFb7WIL+3G3vEBExlb4=";
   release."1.8.0".sha256  = "sha256-4s/4ZZKj5tiTtSHGIM8Op/Pak4Vp52WVOpd4l9m19fY=";
   release."1.7.1".sha256  = "sha256-MCmOzMh/SBTFAoPbbIQ7aqd3hMcSMpAKpiZI7dbRaGs=";
   release."1.7.0".sha256  = "sha256-WqSeuJhmqicJgXw/xGjGvbRzfyOK7rmkVRb6tPDTAZg=";
diff --git a/pkgs/development/coq-modules/iris/default.nix b/pkgs/development/coq-modules/iris/default.nix
index 14410a8cecd0..adcc9c3e5c72 100644
--- a/pkgs/development/coq-modules/iris/default.nix
+++ b/pkgs/development/coq-modules/iris/default.nix
@@ -15,7 +15,7 @@ mkCoqDerivation rec {
     with lib.versions;
     lib.switch coq.coq-version [
       {
-        case = range "8.19" "8.20";
+        case = range "8.19" "9.0";
         out = "4.3.0";
       }
       {
diff --git a/pkgs/development/coq-modules/json/default.nix b/pkgs/development/coq-modules/json/default.nix
index 3b8ccef3bb95..52fd5871f9d1 100644
--- a/pkgs/development/coq-modules/json/default.nix
+++ b/pkgs/development/coq-modules/json/default.nix
@@ -19,7 +19,7 @@
     in
     lib.switch coq.coq-version [
       {
-        case = range "8.14" "8.20";
+        case = range "8.14" "9.0";
         out = "0.2.0";
       }
       {
diff --git a/pkgs/development/coq-modules/mathcomp-algebra-tactics/default.nix b/pkgs/development/coq-modules/mathcomp-algebra-tactics/default.nix
index 3996db951b29..212d1cb03568 100644
--- a/pkgs/development/coq-modules/mathcomp-algebra-tactics/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-algebra-tactics/default.nix
@@ -24,10 +24,10 @@ mkCoqDerivation {
       [
         {
           cases = [
-            (range "8.16" "8.20")
+            (range "8.16" "9.0")
             (isGe "2.0")
           ];
-          out = "1.2.3";
+          out = "1.2.4";
         }
         {
           cases = [
@@ -57,6 +57,7 @@ mkCoqDerivation {
   release."1.1.1".sha256 = "sha256-5wItMeeTRoJlRBH3zBNc2VUZn6pkDde60YAvXTx+J3U=";
   release."1.2.2".sha256 = "sha256-EU9RJGV3BvnmsX+mGH+6+MDXiGHgDI7aP5sIYiMUXTs=";
   release."1.2.3".sha256 = "sha256-6uc1VEfDv+fExEfBR2c0/Q/KjrkX0TbEMCLgeYcpkls=";
+  release."1.2.4".sha256 = "sha256-BRxt0LGPz2u3kJRjcderaZqCfs8M8qKAAwNSWmIck7Q=";
 
   propagatedBuildInputs = [
     mathcomp-algebra
diff --git a/pkgs/development/coq-modules/mathcomp-bigenough/default.nix b/pkgs/development/coq-modules/mathcomp-bigenough/default.nix
index 4a79a3d95d90..86516fd9082d 100644
--- a/pkgs/development/coq-modules/mathcomp-bigenough/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-bigenough/default.nix
@@ -18,14 +18,15 @@ mkCoqDerivation {
   release = {
     "1.0.0".sha256 = "10g0gp3hk7wri7lijkrqna263346wwf6a3hbd4qr9gn8hmsx70wg";
     "1.0.1".sha256 = "sha256:02f4dv4rz72liciwxb2k7acwx6lgqz4381mqyq5854p3nbyn06aw";
+    "1.0.2".sha256 = "sha256-fJ/5xr91VtvpIoaFwb3PlnKl6UHG6GEeBRVGZrVLMU0=";
   };
   inherit version;
   defaultVersion =
     with lib.versions;
     lib.switch coq.version [
       {
-        case = range "8.10" "8.20";
-        out = "1.0.1";
+        case = range "8.10" "9.0";
+        out = "1.0.2";
       }
       {
         case = range "8.5" "8.14";
diff --git a/pkgs/development/coq-modules/mathcomp-finmap/default.nix b/pkgs/development/coq-modules/mathcomp-finmap/default.nix
index f0fb42ddae8a..fe408966797b 100644
--- a/pkgs/development/coq-modules/mathcomp-finmap/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-finmap/default.nix
@@ -22,7 +22,7 @@ mkCoqDerivation {
       [
         {
           cases = [
-            (range "8.16" "8.20")
+            (range "8.16" "9.0")
             (isGe "2.0")
           ];
           out = "2.1.0";
diff --git a/pkgs/development/coq-modules/mathcomp-real-closed/default.nix b/pkgs/development/coq-modules/mathcomp-real-closed/default.nix
index 91a303219b19..7654c47abf08 100644
--- a/pkgs/development/coq-modules/mathcomp-real-closed/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-real-closed/default.nix
@@ -37,14 +37,14 @@ mkCoqDerivation {
       [
         {
           cases = [
-            (isGe "8.17")
+            (range "8.17" "9.0")
             (isGe "2.1.0")
           ];
           out = "2.0.2";
         }
         {
           cases = [
-            (isGe "8.17")
+            (range "8.17" "8.20")
             (isGe "2.0.0")
           ];
           out = "2.0.1";
diff --git a/pkgs/development/coq-modules/mathcomp-tarjan/default.nix b/pkgs/development/coq-modules/mathcomp-tarjan/default.nix
index 945c63657d97..9246a0b0682e 100644
--- a/pkgs/development/coq-modules/mathcomp-tarjan/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-tarjan/default.nix
@@ -24,7 +24,7 @@ mkCoqDerivation {
       [
         {
           cases = [
-            (range "8.16" "8.20")
+            (range "8.16" "9.0")
             (isGe "2.0.0")
           ];
           out = "1.0.2";
diff --git a/pkgs/development/coq-modules/mathcomp-word/default.nix b/pkgs/development/coq-modules/mathcomp-word/default.nix
index 8e6825979be1..84a3345e7066 100644
--- a/pkgs/development/coq-modules/mathcomp-word/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-word/default.nix
@@ -61,7 +61,7 @@ mkCoqDerivation {
       [
         {
           cases = [
-            (range "8.16" "8.20")
+            (range "8.16" "9.0")
             (isGe "2.0")
           ];
           out = "3.2";
diff --git a/pkgs/development/coq-modules/mathcomp-zify/default.nix b/pkgs/development/coq-modules/mathcomp-zify/default.nix
index d6be076ba470..ec0c7cdcaa95 100644
--- a/pkgs/development/coq-modules/mathcomp-zify/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-zify/default.nix
@@ -25,7 +25,7 @@ mkCoqDerivation rec {
       [
         {
           cases = [
-            (range "8.16" "8.20")
+            (range "8.16" "9.0")
             (isGe "2.0.0")
           ];
           out = "1.5.0+2.0+8.16";
diff --git a/pkgs/development/coq-modules/mathcomp/default.nix b/pkgs/development/coq-modules/mathcomp/default.nix
index 48d36b2dbb8c..c4442ba1283c 100644
--- a/pkgs/development/coq-modules/mathcomp/default.nix
+++ b/pkgs/development/coq-modules/mathcomp/default.nix
@@ -20,7 +20,7 @@ let
   withDoc = single && (args.withDoc or false);
   defaultVersion = let inherit (lib.versions) range; in
     lib.switch coq.coq-version [
-      { case = range "8.19" "8.20"; out = "2.3.0"; }
+      { case = range "8.19" "9.0"; out = "2.3.0"; }
       { case = range "8.17" "8.20"; out = "2.2.0"; }
       { case = range "8.17" "8.18"; out = "2.1.0"; }
       { case = range "8.17" "8.18"; out = "2.0.0"; }
diff --git a/pkgs/development/coq-modules/paco/default.nix b/pkgs/development/coq-modules/paco/default.nix
index d4e95619c4ad..97b5061c8e58 100644
--- a/pkgs/development/coq-modules/paco/default.nix
+++ b/pkgs/development/coq-modules/paco/default.nix
@@ -13,7 +13,7 @@ mkCoqDerivation {
   defaultVersion =
     with lib.versions;
     lib.switch coq.coq-version [
-      { case = range "8.13" "8.20"; out = "4.2.2"; }
+      { case = range "8.13" "9.0"; out = "4.2.2"; }
       { case = range "8.12" "8.17"; out = "4.1.2"; }
       { case = range "8.9" "8.13"; out = "4.1.1"; }
       { case = range "8.6" "8.13"; out = "4.0.2"; }
diff --git a/pkgs/development/coq-modules/parsec/default.nix b/pkgs/development/coq-modules/parsec/default.nix
index 4f8eeebc15da..b797fc71e7d6 100644
--- a/pkgs/development/coq-modules/parsec/default.nix
+++ b/pkgs/development/coq-modules/parsec/default.nix
@@ -24,7 +24,7 @@ mkCoqDerivation {
     with lib.versions;
     lib.switch coq.version [
       {
-        case = range "8.14" "8.20";
+        case = range "8.14" "9.0";
         out = "0.2.0";
       }
       {
diff --git a/pkgs/development/coq-modules/reglang/default.nix b/pkgs/development/coq-modules/reglang/default.nix
index 3e95e1b893b1..cd0513a6e02a 100644
--- a/pkgs/development/coq-modules/reglang/default.nix
+++ b/pkgs/development/coq-modules/reglang/default.nix
@@ -24,7 +24,7 @@ mkCoqDerivation {
       [
         {
           cases = [
-            (range "8.16" "8.20")
+            (range "8.16" "9.0")
             (isGe "2.0.0")
           ];
           out = "1.2.1";
diff --git a/pkgs/development/coq-modules/simple-io/default.nix b/pkgs/development/coq-modules/simple-io/default.nix
index 6345818db5d0..bb4443433e12 100644
--- a/pkgs/development/coq-modules/simple-io/default.nix
+++ b/pkgs/development/coq-modules/simple-io/default.nix
@@ -16,7 +16,7 @@
     with lib.versions;
     lib.switch coq.coq-version [
       {
-        case = range "8.17" "8.20";
+        case = range "8.17" "9.0";
         out = "1.10.0";
       }
       {
diff --git a/pkgs/development/coq-modules/stdlib/default.nix b/pkgs/development/coq-modules/stdlib/default.nix
index a443daef68f1..cac0c4b53405 100644
--- a/pkgs/development/coq-modules/stdlib/default.nix
+++ b/pkgs/development/coq-modules/stdlib/default.nix
@@ -14,17 +14,13 @@
   inherit version;
   defaultVersion =
     with lib.versions;
-    lib.switch
-      [ coq.version ]
-      [
-        {
-          cases = [ (isLt "8.21") ];
-          out = "8.20";
-        }
-      ]
-      null;
-  releaseRev = v: "v${v}";
+    lib.switch coq.version [
+      { case = isEq "9.0"; out = "9.0+rc1"; }
+      { case = isLt "8.21"; out = "8.20"; }
+    ] null;
+  releaseRev = v: "V${v}";
 
+  release."9.0+rc1".sha256 = "sha256-raHwniQdpAX1HGlMofM8zVeXcmlUs+VJZZg5VF43k/M=";
   release."8.20".sha256 = "sha256-AcoS4edUYCfJME1wx8UbuSQRF3jmxhArcZyPIoXcfu0=";
 
   useDune = true;
diff --git a/pkgs/development/coq-modules/stdpp/default.nix b/pkgs/development/coq-modules/stdpp/default.nix
index 750388750b6b..13a24d1600f7 100644
--- a/pkgs/development/coq-modules/stdpp/default.nix
+++ b/pkgs/development/coq-modules/stdpp/default.nix
@@ -15,7 +15,7 @@ mkCoqDerivation rec {
     with lib.versions;
     lib.switch coq.coq-version [
       {
-        case = range "8.19" "8.20";
+        case = range "8.19" "9.0";
         out = "1.11.0";
       }
       {
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 6b27d548a1a4..18a9a9d8e9ca 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -17142,6 +17142,7 @@ with pkgs;
     coqPackages_8_18 coq_8_18
     coqPackages_8_19 coq_8_19
     coqPackages_8_20 coq_8_20
+    coqPackages_9_0 coq_9_0
     coqPackages      coq
   ;
 
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index 87bf3a7b7a7f..8e6ac8cafe4c 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -235,6 +235,7 @@ in rec {
   coq_8_18 = mkCoq "8.18";
   coq_8_19 = mkCoq "8.19";
   coq_8_20 = mkCoq "8.20";
+  coq_9_0 = mkCoq "9.0";
 
   coqPackages_8_5 = mkCoqPackages coq_8_5;
   coqPackages_8_6 = mkCoqPackages coq_8_6;
@@ -252,6 +253,7 @@ in rec {
   coqPackages_8_18 = mkCoqPackages coq_8_18;
   coqPackages_8_19 = mkCoqPackages coq_8_19;
   coqPackages_8_20 = mkCoqPackages coq_8_20;
+  coqPackages_9_0 = mkCoqPackages coq_9_0;
 
   coqPackages = recurseIntoAttrs coqPackages_8_20;
   coq = coqPackages.coq;