diff --git a/pkgs/development/coq-modules/coqeal/default.nix b/pkgs/development/coq-modules/coqeal/default.nix
index 08f1ad8c473d..603d2be00601 100644
--- a/pkgs/development/coq-modules/coqeal/default.nix
+++ b/pkgs/development/coq-modules/coqeal/default.nix
@@ -23,7 +23,7 @@ let
         [
           {
             cases = [
-              (range "9.0" "9.0")
+              (range "8.20" "9.0")
               (isGe "2.3.0")
             ];
             out = "2.1.0";
diff --git a/pkgs/development/coq-modules/deriving/default.nix b/pkgs/development/coq-modules/deriving/default.nix
index 30cb78815193..6f32bca2aad9 100644
--- a/pkgs/development/coq-modules/deriving/default.nix
+++ b/pkgs/development/coq-modules/deriving/default.nix
@@ -20,14 +20,14 @@ mkCoqDerivation {
         {
           cases = [
             (range "8.17" "9.0")
-            (isGe "2.0.0")
+            (range "2.0.0" "2.3.0")
           ];
           out = "0.2.1";
         }
         {
           cases = [
             (range "8.17" "8.20")
-            (isGe "2.0.0")
+            (range "2.0.0" "2.2.0")
           ];
           out = "0.2.0";
         }
diff --git a/pkgs/development/coq-modules/extructures/default.nix b/pkgs/development/coq-modules/extructures/default.nix
index 270c6146fe3e..6cba886a4349 100644
--- a/pkgs/development/coq-modules/extructures/default.nix
+++ b/pkgs/development/coq-modules/extructures/default.nix
@@ -20,14 +20,14 @@
         {
           cases = [
             (range "8.17" "9.0")
-            (isGe "2.0.0")
+            (range "2.0.0" "2.3.0")
           ];
           out = "0.5.0";
         }
         {
           cases = [
             (range "8.17" "8.20")
-            (isGe "2.0.0")
+            (range "2.0.0" "2.3.0")
           ];
           out = "0.4.0";
         }
diff --git a/pkgs/development/coq-modules/graph-theory/default.nix b/pkgs/development/coq-modules/graph-theory/default.nix
index 1f0b0eb41f28..4a5e8c914364 100644
--- a/pkgs/development/coq-modules/graph-theory/default.nix
+++ b/pkgs/development/coq-modules/graph-theory/default.nix
@@ -6,7 +6,7 @@
   mathcomp-finmap,
   mathcomp-algebra-tactics,
   fourcolor,
-  hierarchy-builder,
+  stdlib,
   version ? null,
 }:
 
@@ -71,7 +71,7 @@ mkCoqDerivation {
     mathcomp.fingroup
     mathcomp-algebra-tactics
     fourcolor
-    hierarchy-builder
+    stdlib
   ];
 
   meta = with lib; {
diff --git a/pkgs/development/coq-modules/jasmin/default.nix b/pkgs/development/coq-modules/jasmin/default.nix
index ec542b6815af..73ee3dd6d317 100644
--- a/pkgs/development/coq-modules/jasmin/default.nix
+++ b/pkgs/development/coq-modules/jasmin/default.nix
@@ -21,7 +21,7 @@ mkCoqDerivation {
         {
           cases = [
             (range "8.19" "9.0")
-            (range "2.2" "2.3")
+            (range "2.2" "2.4")
           ];
           out = "2025.02.0";
         }
diff --git a/pkgs/development/coq-modules/mathcomp-finmap/default.nix b/pkgs/development/coq-modules/mathcomp-finmap/default.nix
index 8e3245c619a1..791fcc40bcbb 100644
--- a/pkgs/development/coq-modules/mathcomp-finmap/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-finmap/default.nix
@@ -23,7 +23,7 @@ mkCoqDerivation {
         {
           cases = [
             (range "8.16" "9.0")
-            (isGe "2.0")
+            (range "2.0" "2.3")
           ];
           out = "2.1.0";
         }
diff --git a/pkgs/development/coq-modules/mathcomp-tarjan/default.nix b/pkgs/development/coq-modules/mathcomp-tarjan/default.nix
index 9246a0b0682e..1839f52099c3 100644
--- a/pkgs/development/coq-modules/mathcomp-tarjan/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-tarjan/default.nix
@@ -25,7 +25,7 @@ mkCoqDerivation {
         {
           cases = [
             (range "8.16" "9.0")
-            (isGe "2.0.0")
+            (range "2.0.0" "2.3.0")
           ];
           out = "1.0.2";
         }
diff --git a/pkgs/development/coq-modules/mathcomp/default.nix b/pkgs/development/coq-modules/mathcomp/default.nix
index b9cc26880506..963fd6e2b6d2 100644
--- a/pkgs/development/coq-modules/mathcomp/default.nix
+++ b/pkgs/development/coq-modules/mathcomp/default.nix
@@ -34,6 +34,10 @@ let
       inherit (lib.versions) range;
     in
     lib.switch coq.coq-version [
+      {
+        case = range "8.20" "9.0";
+        out = "2.4.0";
+      }
       {
         case = range "8.19" "9.0";
         out = "2.3.0";
@@ -108,6 +112,7 @@ let
       }
     ] null;
   release = {
+    "2.4.0".sha256 = "sha256-A1XgLLwZRvKS8QyceCkSQa7ue6TYyf5fMft5gSx9NOs=";
     "2.3.0".sha256 = "sha256-wa6OBig8rhAT4iwupSylyCAMhO69rADa0MQIX5zzL+Q=";
     "2.2.0".sha256 = "sha256-SPyWSI5kIP5w7VpgnQ4vnK56yEuWnJylNQOT7M77yoQ=";
     "2.1.0".sha256 = "sha256-XDLx0BIkVRkSJ4sGCIE51j3rtkSGemNTs/cdVmTvxqo=";
diff --git a/pkgs/development/coq-modules/multinomials/default.nix b/pkgs/development/coq-modules/multinomials/default.nix
index 1817d4011199..78baab677937 100644
--- a/pkgs/development/coq-modules/multinomials/default.nix
+++ b/pkgs/development/coq-modules/multinomials/default.nix
@@ -27,7 +27,7 @@ mkCoqDerivation {
         {
           cases = [
             (range "8.17" "9.0")
-            (isGe "2.1.0")
+            (range "2.1.0" "2.3.0")
           ];
           out = "2.3.0";
         }
diff --git a/pkgs/development/coq-modules/reglang/default.nix b/pkgs/development/coq-modules/reglang/default.nix
index fdb9ed07774b..cb1a070d488c 100644
--- a/pkgs/development/coq-modules/reglang/default.nix
+++ b/pkgs/development/coq-modules/reglang/default.nix
@@ -26,7 +26,7 @@ mkCoqDerivation {
         {
           cases = [
             (range "8.16" "9.0")
-            (isGe "2.0.0")
+            (range "2.0.0" "2.3.0")
           ];
           out = "1.2.1";
         }
diff --git a/pkgs/development/coq-modules/ssprove/default.nix b/pkgs/development/coq-modules/ssprove/default.nix
index c3db4a8be0e5..876a0537cb40 100644
--- a/pkgs/development/coq-modules/ssprove/default.nix
+++ b/pkgs/development/coq-modules/ssprove/default.nix
@@ -24,7 +24,7 @@
         {
           cases = [
             (range "8.18" "8.20")
-            "2.3.0"
+            (range "2.3.0" "2.3.0")
           ];
           out = "0.2.3";
         }