From 19e4869241080cea1a831a05c0298b61de944695 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Sun, 29 Jun 2025 16:35:20 +0200
Subject: [PATCH] coqPackages.*: better formatting fix

---
 .../coq-modules/bignums/default.nix           | 15 +++---
 .../coq-modules/coq-elpi/default.nix          | 52 ++++++++++---------
 .../coq-modules/coqeal/default.nix            | 42 ++++++++-------
 .../coq-modules/coquelicot/default.nix        | 23 ++++----
 .../coq-modules/deriving/default.nix          | 30 ++++++-----
 .../coq-modules/dpdgraph/default.nix          | 38 +++++++-------
 .../coq-modules/equations/default.nix         | 42 ++++++++-------
 .../coq-modules/extructures/default.nix       | 32 +++++++-----
 .../development/coq-modules/flocq/default.nix | 23 ++++----
 .../coq-modules/fourcolor/default.nix         | 32 +++++++-----
 pkgs/development/coq-modules/gaia/default.nix | 30 ++++++-----
 .../coq-modules/graph-theory/default.nix      | 34 ++++++------
 .../coq-modules/hierarchy-builder/default.nix | 27 +++++-----
 pkgs/development/coq-modules/http/default.nix | 11 ++--
 .../coq-modules/hydra-battles/default.nix     | 13 ++---
 .../coq-modules/interval/default.nix          | 29 ++++++-----
 pkgs/development/coq-modules/iris/default.nix | 23 ++++----
 .../coq-modules/itauto/default.nix            | 25 ++++-----
 .../coq-modules/itree-io/default.nix          | 11 ++--
 .../coq-modules/jasmin/default.nix            | 26 ++++++----
 pkgs/development/coq-modules/json/default.nix | 13 +++--
 .../coq-modules/mathcomp-abel/default.nix     | 28 +++++-----
 .../mathcomp-algebra-tactics/default.nix      | 32 +++++++-----
 .../coq-modules/mathcomp-analysis/default.nix | 52 ++++++++++---------
 .../coq-modules/mathcomp-apery/default.nix    | 24 +++++----
 .../mathcomp-bigenough/default.nix            | 13 ++---
 .../coq-modules/mathcomp-finmap/default.nix   | 44 +++++++++-------
 .../coq-modules/mathcomp-infotheo/default.nix | 42 ++++++++-------
 .../coq-modules/mathcomp-tarjan/default.nix   | 30 ++++++-----
 .../coq-modules/mathcomp-word/default.nix     | 26 ++++++----
 .../coq-modules/mathcomp-zify/default.nix     | 28 +++++-----
 .../coq-modules/mathcomp/default.nix          | 47 ++++++++---------
 .../coq-modules/metacoq/default.nix           | 32 ++++++------
 .../coq-modules/metarocq/default.nix          | 12 +++--
 .../coq-modules/multinomials/default.nix      | 48 +++++++++--------
 .../coq-modules/odd-order/default.nix         | 19 +++----
 .../coq-modules/reglang/default.nix           | 30 ++++++-----
 .../coq-modules/relation-algebra/default.nix  | 31 +++++------
 .../coq-modules/simple-io/default.nix         | 15 +++---
 .../coq-modules/ssprove/default.nix           | 32 +++++++-----
 .../coq-modules/stalmarck/default.nix         | 11 ++--
 .../coq-modules/stdlib/default.nix            | 13 ++---
 .../development/coq-modules/stdpp/default.nix | 23 ++++----
 .../rocq-modules/bignums/default.nix          | 11 ++--
 .../hierarchy-builder/default.nix             | 11 ++--
 .../rocq-modules/rocq-elpi/default.nix        | 26 +++++-----
 .../rocq-modules/stdlib/default.nix           | 11 ++--
 47 files changed, 681 insertions(+), 581 deletions(-)

diff --git a/pkgs/development/coq-modules/bignums/default.nix b/pkgs/development/coq-modules/bignums/default.nix
index 6d38525921cf..24acbd14655c 100644
--- a/pkgs/development/coq-modules/bignums/default.nix
+++ b/pkgs/development/coq-modules/bignums/default.nix
@@ -12,14 +12,15 @@
   owner = "coq";
   inherit version;
   defaultVersion =
+    let
+      case = case: out: { inherit case out; };
+    in
     with lib.versions;
-    lib.switch coq.coq-version (lib.lists.sort (x: y: isLe x.out y.out) (
-      lib.mapAttrsToList (out: case: { inherit case out; }) {
-        "9.0.0+rocq${coq.coq-version}" = range "9.0" "9.0";
-        "9.0.0+coq${coq.coq-version}" = range "8.13" "8.20";
-        "${coq.coq-version}.0" = range "8.6" "8.17";
-      }
-    )) null;
+    lib.switch coq.coq-version [
+      (case (range "9.0" "9.0") "9.0.0+rocq${coq.coq-version}")
+      (case (range "8.13" "8.20") "9.0.0+coq${coq.coq-version}")
+      (case (range "8.6" "8.17") "${coq.coq-version}.0")
+    ] null;
 
   release."9.0.0+rocq9.0".sha256 = "sha256-ctnwpyNVhryEUA5YEsAImrcJsNMhtBgDSOz+z5Z4R78=";
   release."9.0.0+coq8.20".sha256 = "sha256-pkvyDaMXRalc6Uu1eBTuiqTpRauRrzu946c6TavyTKY=";
diff --git a/pkgs/development/coq-modules/coq-elpi/default.nix b/pkgs/development/coq-modules/coq-elpi/default.nix
index baa817b33138..f6308faaf34c 100644
--- a/pkgs/development/coq-modules/coq-elpi/default.nix
+++ b/pkgs/development/coq-modules/coq-elpi/default.nix
@@ -15,18 +15,19 @@ let
       elpi-version
     else
       (
+        let
+          case = case: out: { inherit case out; };
+        in
         with lib.versions;
-        lib.switch coq.coq-version (lib.lists.sort (x: y: lib.versions.isLe x.out y.out) (
-          lib.mapAttrsToList (out: case: { inherit case out; }) {
-            "1.11.4" = "8.11";
-            "1.12.0" = "8.12";
-            "1.13.7" = range "8.13" "8.14";
-            "1.15.0" = "8.15";
-            "1.17.0" = range "8.16" "8.17";
-            "1.18.1" = range "8.18" "8.19";
-            "2.0.7" = range "8.20" "9.0";
-          }
-        )) { }
+        lib.switch coq.coq-version [
+          (case "8.11" "1.11.4")
+          (case "8.12" "1.12.0")
+          (case (range "8.13" "8.14") "1.13.7")
+          (case "8.15" "1.15.0")
+          (case (range "8.16" "8.17") "1.17.0")
+          (case (range "8.18" "8.19") "1.18.1")
+          (case (range "8.20" "9.0") "2.0.7")
+        ] { }
       );
   elpi = coq.ocamlPackages.elpi.override { version = default-elpi-version; };
   propagatedBuildInputs_wo_elpi = [
@@ -38,21 +39,22 @@ let
     owner = "LPCIC";
     inherit version;
     defaultVersion =
+      let
+        case = case: out: { inherit case out; };
+      in
       with lib.versions;
-      lib.switch coq.coq-version (lib.lists.sort (x: y: lib.versions.isLe x.out y.out) (
-        lib.mapAttrsToList (out: case: { inherit case out; }) {
-          "2.5.2" = range "8.20" "9.0";
-          "2.0.1" = "8.19";
-          "2.0.0" = "8.18";
-          "1.18.0" = "8.17";
-          "1.15.6" = "8.16";
-          "1.14.0" = "8.15";
-          "1.11.2" = "8.14";
-          "1.11.1" = "8.13";
-          "1.8.3_8.12" = "8.12";
-          "1.6.3_8.11" = "8.11";
-        }
-      )) null;
+      lib.switch coq.coq-version [
+        (case (range "8.20" "9.0") "2.5.2")
+        (case "8.19" "2.0.1")
+        (case "8.18" "2.0.0")
+        (case "8.17" "1.18.0")
+        (case "8.16" "1.15.6")
+        (case "8.15" "1.14.0")
+        (case "8.14" "1.11.2")
+        (case "8.13" "1.11.1")
+        (case "8.12" "1.8.3_8.12")
+        (case "8.11" "1.6.3_8.11")
+      ] null;
     release."2.5.2".sha256 = "sha256-lLzjPrbVB3rrqox528YiheUb0u89R84Xmrgkn0oplOs=";
     release."2.5.0".sha256 = "sha256-Z5xjO83X/ZoTQlWnVupGXPH3HuJefr57Kv128I0dltg=";
     release."2.4.0".sha256 = "sha256-W2+vVGExLLux8e0nSZESSoMVvrLxhL6dmXkb+JuKiqc=";
diff --git a/pkgs/development/coq-modules/coqeal/default.nix b/pkgs/development/coq-modules/coqeal/default.nix
index 7b0d58845adb..ead8be66918d 100644
--- a/pkgs/development/coq-modules/coqeal/default.nix
+++ b/pkgs/development/coq-modules/coqeal/default.nix
@@ -17,27 +17,31 @@ let
 
     inherit version;
     defaultVersion =
-      with lib.versions;
       let
-        cmc = c: mc: [
-          c
-          mc
-        ];
+        case = coq: mc: out: {
+          case = [
+            coq
+            mc
+          ];
+          inherit out;
+        };
       in
-      lib.switch [ coq.coq-version mathcomp.version ] (lib.lists.sort (x: y: isLe x.out y.out) (
-        lib.mapAttrsToList (out: cases: { inherit cases out; }) {
-          "2.1.0" = cmc (range "8.20" "9.0") (isGe "2.3.0");
-          "2.0.3" = cmc (range "8.16" "8.20") (isGe "2.1.0");
-          "2.0.1" = cmc (range "8.16" "8.20") (isGe "2.0.0");
-          "2.0.0" = cmc (range "8.16" "8.17") (isGe "2.0.0");
-          "1.1.3" = cmc (range "8.15" "8.18") (range "1.15.0" "1.18.0");
-          "1.1.1" = cmc (range "8.13" "8.17") (range "1.13.0" "1.18.0");
-          "1.1.0" = cmc (range "8.10" "8.15") (range "1.12.0" "1.18.0");
-          "1.0.5" = cmc (isGe "8.10") (range "1.11.0" "1.12.0");
-          "1.0.4" = cmc (isGe "8.7") "1.11.0";
-          "1.0.3" = cmc (isGe "8.7") "1.10.0";
-        }
-      )) null;
+      with lib.versions;
+      lib.switch
+        [ coq.coq-version mathcomp.version ]
+        [
+          (case (range "8.20" "9.0") (isGe "2.3.0") "2.1.0")
+          (case (range "8.16" "8.20") (isGe "2.1.0") "2.0.3")
+          (case (range "8.16" "8.20") (isGe "2.0.0") "2.0.1")
+          (case (range "8.16" "8.17") (isGe "2.0.0") "2.0.0")
+          (case (range "8.15" "8.18") (range "1.15.0" "1.18.0") "1.1.3")
+          (case (range "8.13" "8.17") (range "1.13.0" "1.18.0") "1.1.1")
+          (case (range "8.10" "8.15") (range "1.12.0" "1.18.0") "1.1.0")
+          (case (isGe "8.10") (range "1.11.0" "1.12.0") "1.0.5")
+          (case (isGe "8.7") "1.11.0" "1.0.4")
+          (case (isGe "8.7") "1.10.0" "1.0.3")
+        ]
+        null;
 
     release."2.1.0".sha256 = "sha256-UoDxy2BKraDyRsO42GXRo26O74OF51biZQGkIMWLf8Y=";
     release."2.0.3".sha256 = "sha256-5lDq7IWlEW0EkNzYPu+dA6KOvRgy53W/alikpDr/Kd0=";
diff --git a/pkgs/development/coq-modules/coquelicot/default.nix b/pkgs/development/coq-modules/coquelicot/default.nix
index 274f41d111ad..b9f3ff50a27c 100644
--- a/pkgs/development/coq-modules/coquelicot/default.nix
+++ b/pkgs/development/coq-modules/coquelicot/default.nix
@@ -14,18 +14,19 @@ mkCoqDerivation {
   domain = "gitlab.inria.fr";
   inherit version;
   defaultVersion =
+    let
+      case = case: out: { inherit case out; };
+    in
     with lib.versions;
-    lib.switch coq.coq-version (lib.lists.sort (x: y: isLe x.out y.out) (
-      lib.mapAttrsToList (out: case: { inherit case out; }) {
-        "3.4.3" = range "8.12" "9.0";
-        "3.4.2" = range "8.12" "8.20";
-        "3.4.0" = range "8.12" "8.18";
-        "3.3.0" = range "8.12" "8.17";
-        "3.2.0" = range "8.8" "8.16";
-        "3.1.0" = range "8.8" "8.13";
-        "3.0.2" = range "8.5" "8.9";
-      }
-    )) null;
+    lib.switch coq.coq-version [
+      (case (range "8.12" "9.0") "3.4.3")
+      (case (range "8.12" "8.20") "3.4.2")
+      (case (range "8.12" "8.18") "3.4.0")
+      (case (range "8.12" "8.17") "3.3.0")
+      (case (range "8.8" "8.16") "3.2.0")
+      (case (range "8.8" "8.13") "3.1.0")
+      (case (range "8.5" "8.9") "3.0.2")
+    ] null;
   release."3.4.3".sha256 = "sha256-bzzAIENU2OYTtmdBU9Xw8zyBvz9vqTiqjWSm7RnXXRA=";
   release."3.4.2".sha256 = "sha256-aBTF8ZKu67Rb3ryCqFyejUXf/65KgG8i5je/ZMFSrj4=";
   release."3.4.1".sha256 = "sha256-REhvIBl3EaL8CQqI34Gn7Xjf9NhPI3nrUAO26pSLbm0=";
diff --git a/pkgs/development/coq-modules/deriving/default.nix b/pkgs/development/coq-modules/deriving/default.nix
index 0dffe5e50e41..f2b61dccf5ba 100644
--- a/pkgs/development/coq-modules/deriving/default.nix
+++ b/pkgs/development/coq-modules/deriving/default.nix
@@ -13,21 +13,25 @@ mkCoqDerivation {
 
   inherit version;
   defaultVersion =
-    with lib.versions;
     let
-      cmc = c: mc: [
-        c
-        mc
-      ];
+      case = coq: mc: out: {
+        case = [
+          coq
+          mc
+        ];
+        inherit out;
+      };
     in
-    lib.switch [ coq.coq-version ssreflect.version ] (lib.lists.sort (x: y: isLe x.out y.out) (
-      lib.mapAttrsToList (out: cases: { inherit cases out; }) {
-        "0.2.2" = cmc (range "8.17" "9.0") (range "2.0.0" "2.4.0");
-        "0.2.1" = cmc (range "8.17" "9.0") (range "2.0.0" "2.3.0");
-        "0.2.0" = cmc (range "8.17" "8.20") (range "2.0.0" "2.2.0");
-        "0.1.1" = cmc (range "8.11" "8.20") (isLe "2.0.0");
-      }
-    )) null;
+    with lib.versions;
+    lib.switch
+      [ coq.coq-version ssreflect.version ]
+      [
+        (case (range "8.17" "9.0") (range "2.0.0" "2.4.0") "0.2.2")
+        (case (range "8.17" "9.0") (range "2.0.0" "2.3.0") "0.2.1")
+        (case (range "8.17" "8.20") (range "2.0.0" "2.2.0") "0.2.0")
+        (case (range "8.11" "8.20") (isLe "2.0.0") "0.1.1")
+      ]
+      null;
 
   releaseRev = v: "v${v}";
 
diff --git a/pkgs/development/coq-modules/dpdgraph/default.nix b/pkgs/development/coq-modules/dpdgraph/default.nix
index d48290887f22..936e2f892f58 100644
--- a/pkgs/development/coq-modules/dpdgraph/default.nix
+++ b/pkgs/development/coq-modules/dpdgraph/default.nix
@@ -15,24 +15,26 @@ mkCoqDerivation {
   owner = "Karmaki";
   repo = "coq-dpdgraph";
   inherit version;
-  defaultVersion = lib.switch coq.coq-version (lib.lists.sort (x: y: lib.versions.isLe x.out y.out) (
-    lib.mapAttrsToList (out: case: { inherit case out; }) {
-      "1.0+8.20" = "8.20";
-      "1.0+8.19" = "8.19";
-      "1.0+8.18" = "8.18";
-      "1.0+8.17" = "8.17";
-      "1.0+8.16" = "8.16";
-      "1.0+8.15" = "8.15";
-      "1.0+8.14" = "8.14";
-      "1.0+8.13" = "8.13";
-      "0.6.8" = "8.12";
-      "0.6.7" = "8.11";
-      "0.6.6" = "8.10";
-      "0.6.5" = "8.9";
-      "0.6.3" = "8.8";
-      "0.6.2" = "8.7";
-    }
-  )) null;
+  defaultVersion =
+    let
+      case = case: out: { inherit case out; };
+    in
+    lib.switch coq.coq-version [
+      (case "8.20" "1.0+8.20")
+      (case "8.19" "1.0+8.19")
+      (case "8.18" "1.0+8.18")
+      (case "8.17" "1.0+8.17")
+      (case "8.16" "1.0+8.16")
+      (case "8.15" "1.0+8.15")
+      (case "8.14" "1.0+8.14")
+      (case "8.13" "1.0+8.13")
+      (case "8.12" "0.6.8")
+      (case "8.11" "0.6.7")
+      (case "8.10" "0.6.6")
+      (case "8.9" "0.6.5")
+      (case "8.8" "0.6.3")
+      (case "8.7" "0.6.2")
+    ] null;
 
   release."1.0+8.20".sha256 = "sha256-szfH/OksCH3SCbcFjwEvLwHE5avmHp1vYiJM6KAXFqs=";
   release."1.0+8.19".sha256 = "sha256-L1vjEydYiwDFTXES3sgfdaO/D50AbTJKBXUKUCgbpto=";
diff --git a/pkgs/development/coq-modules/equations/default.nix b/pkgs/development/coq-modules/equations/default.nix
index 0ab9f55039ed..9c415098e663 100644
--- a/pkgs/development/coq-modules/equations/default.nix
+++ b/pkgs/development/coq-modules/equations/default.nix
@@ -12,26 +12,28 @@
   repo = "Coq-Equations";
   opam-name = "rocq-equations";
   inherit version;
-  defaultVersion = lib.switch coq.coq-version (lib.lists.sort (x: y: lib.versions.isLe x.out y.out) (
-    lib.mapAttrsToList (out: case: { inherit case out; }) {
-      "1.3.1+9.0" = "9.0";
-      "1.3.1+8.20" = "8.20";
-      "1.3+8.19" = "8.19";
-      "1.3+8.18" = "8.18";
-      "1.3+8.17" = "8.17";
-      "1.3+8.16" = "8.16";
-      "1.3+8.15" = "8.15";
-      "1.3+8.14" = "8.14";
-      "1.3+8.13" = "8.13";
-      "1.2.4+coq8.12" = "8.12";
-      "1.2.4+coq8.11" = "8.11";
-      "1.2.1+coq8.10-2" = "8.10";
-      "1.2.1+coq8.9" = "8.9";
-      "1.2+coq8.8" = "8.8";
-      "1.0+coq8.7" = "8.7";
-      "1.0+coq8.6" = "8.6";
-    }
-  )) null;
+  defaultVersion =
+    let
+      case = case: out: { inherit case out; };
+    in
+    lib.switch coq.coq-version [
+      (case "9.0" "1.3.1+9.0")
+      (case "8.20" "1.3.1+8.20")
+      (case "8.19" "1.3+8.19")
+      (case "8.18" "1.3+8.18")
+      (case "8.17" "1.3+8.17")
+      (case "8.16" "1.3+8.16")
+      (case "8.15" "1.3+8.15")
+      (case "8.14" "1.3+8.14")
+      (case "8.13" "1.3+8.13")
+      (case "8.12" "1.2.4+coq8.12")
+      (case "8.11" "1.2.4+coq8.11")
+      (case "8.10" "1.2.1+coq8.10-2")
+      (case "8.9" "1.2.1+coq8.9")
+      (case "8.8" "1.2+coq8.8")
+      (case "8.7" "1.0+coq8.7")
+      (case "8.6" "1.0+coq8.6")
+    ] null;
 
   release."1.0+coq8.6".version = "1.0";
   release."1.0+coq8.6".rev = "v1.0";
diff --git a/pkgs/development/coq-modules/extructures/default.nix b/pkgs/development/coq-modules/extructures/default.nix
index 0635ea5f05e2..bab84dfc86b1 100644
--- a/pkgs/development/coq-modules/extructures/default.nix
+++ b/pkgs/development/coq-modules/extructures/default.nix
@@ -13,22 +13,26 @@
 
   inherit version;
   defaultVersion =
-    with lib.versions;
     let
-      cmc = c: mc: [
-        c
-        mc
-      ];
+      case = coq: mc: out: {
+        case = [
+          coq
+          mc
+        ];
+        inherit out;
+      };
     in
-    lib.switch [ coq.coq-version mathcomp-boot.version ] (lib.lists.sort (x: y: isLe x.out y.out) (
-      lib.mapAttrsToList (out: cases: { inherit cases out; }) {
-        "0.5.0" = cmc (range "8.17" "9.0") (range "2.0.0" "2.4.0");
-        "0.4.0" = cmc (range "8.17" "8.20") (range "2.0.0" "2.3.0");
-        "0.3.1" = cmc (range "8.11" "8.20") (range "1.12.0" "1.19.0");
-        "0.3.0" = cmc (range "8.11" "8.14") (isLe "1.12.0");
-        "0.2.2" = cmc (range "8.10" "8.12") (isLe "1.12.0");
-      }
-    )) null;
+    with lib.versions;
+    lib.switch
+      [ coq.coq-version mathcomp-boot.version ]
+      [
+        (case (range "8.17" "9.0") (range "2.0.0" "2.4.0") "0.5.0")
+        (case (range "8.17" "8.20") (range "2.0.0" "2.3.0") "0.4.0")
+        (case (range "8.11" "8.20") (range "1.12.0" "1.19.0") "0.3.1")
+        (case (range "8.11" "8.14") (isLe "1.12.0") "0.3.0")
+        (case (range "8.10" "8.12") (isLe "1.12.0") "0.2.2")
+      ]
+      null;
 
   releaseRev = v: "v${v}";
 
diff --git a/pkgs/development/coq-modules/flocq/default.nix b/pkgs/development/coq-modules/flocq/default.nix
index 9f83232d6504..1d7871089fa9 100644
--- a/pkgs/development/coq-modules/flocq/default.nix
+++ b/pkgs/development/coq-modules/flocq/default.nix
@@ -14,18 +14,19 @@ mkCoqDerivation {
   domain = "gitlab.inria.fr";
   inherit version;
   defaultVersion =
+    let
+      case = case: out: { inherit case out; };
+    in
     with lib.versions;
-    lib.switch coq.coq-version (lib.lists.sort (x: y: isLe x.out y.out) (
-      lib.mapAttrsToList (out: case: { inherit case out; }) {
-        "4.2.1" = range "8.15" "9.0";
-        "4.2.0" = range "8.14" "8.20";
-        "4.1.3" = range "8.14" "8.18";
-        "4.1.1" = range "8.14" "8.17";
-        "4.1.0" = range "8.14" "8.16";
-        "3.4.3" = range "8.7" "8.15";
-        "2.6.1" = range "8.5" "8.8";
-      }
-    )) null;
+    lib.switch coq.coq-version [
+      (case (range "8.15" "9.0") "4.2.1")
+      (case (range "8.14" "8.20") "4.2.0")
+      (case (range "8.14" "8.18") "4.1.3")
+      (case (range "8.14" "8.17") "4.1.1")
+      (case (range "8.14" "8.16") "4.1.0")
+      (case (range "8.7" "8.15") "3.4.3")
+      (case (range "8.5" "8.8") "2.6.1")
+    ] null;
   release."4.2.1".sha256 = "sha256-W5hcAm0GGmNsvre79/iGNcoBwFzStC4G177hZ3ds/4E=";
   release."4.2.0".sha256 = "sha256-uTeo4GCs6wTLN3sLKsj0xLlt1fUDYfozXtq6iooLUgM=";
   release."4.1.4".sha256 = "sha256-Use6Mlx79yef1CkCPyGoOItsD69B9KR+mQArCtmre4s=";
diff --git a/pkgs/development/coq-modules/fourcolor/default.nix b/pkgs/development/coq-modules/fourcolor/default.nix
index 10f11f7f236b..f55e55ffd5b3 100644
--- a/pkgs/development/coq-modules/fourcolor/default.nix
+++ b/pkgs/development/coq-modules/fourcolor/default.nix
@@ -22,22 +22,26 @@ mkCoqDerivation {
 
   inherit version;
   defaultVersion =
-    with lib.versions;
     let
-      cmc = c: mc: [
-        c
-        mc
-      ];
+      case = coq: mc: out: {
+        case = [
+          coq
+          mc
+        ];
+        inherit out;
+      };
     in
-    lib.switch [ coq.coq-version mathcomp.version ] (lib.lists.sort (x: y: isLe x.out y.out) (
-      lib.mapAttrsToList (out: cases: { inherit cases out; }) {
-        "1.4.1" = cmc (isGe "8.16") (isGe "2.0");
-        "1.3.0" = cmc (isGe "8.16") "2.0.0";
-        "1.2.5" = cmc (isGe "8.11") (range "1.12" "1.19");
-        "1.2.4" = cmc (isGe "8.11") (range "1.11" "1.14");
-        "1.2.3" = cmc (isLe "8.13") (lib.pred.inter (isGe "1.11.0") (isLt "1.13"));
-      }
-    )) null;
+    with lib.versions;
+    lib.switch
+      [ coq.coq-version mathcomp.version ]
+      [
+        (case (isGe "8.16") (isGe "2.0") "1.4.1")
+        (case (isGe "8.16") "2.0.0" "1.3.0")
+        (case (isGe "8.11") (range "1.12" "1.19") "1.2.5")
+        (case (isGe "8.11") (range "1.11" "1.14") "1.2.4")
+        (case (isLe "8.13") (lib.pred.inter (isGe "1.11.0") (isLt "1.13")) "1.2.3")
+      ]
+      null;
 
   propagatedBuildInputs = [
     mathcomp.boot
diff --git a/pkgs/development/coq-modules/gaia/default.nix b/pkgs/development/coq-modules/gaia/default.nix
index 3157176a6e4b..bc69b24b09cb 100644
--- a/pkgs/development/coq-modules/gaia/default.nix
+++ b/pkgs/development/coq-modules/gaia/default.nix
@@ -22,21 +22,25 @@ mkCoqDerivation {
 
   inherit version;
   defaultVersion =
-    with lib.versions;
     let
-      cmc = c: mc: [
-        c
-        mc
-      ];
+      case = coq: mc: out: {
+        case = [
+          coq
+          mc
+        ];
+        inherit out;
+      };
     in
-    lib.switch [ coq.coq-version mathcomp.version ] (lib.lists.sort (x: y: isLe x.out y.out) (
-      lib.mapAttrsToList (out: cases: { inherit cases out; }) {
-        "2.3" = cmc (range "8.16" "9.0") (range "2.0" "2.4");
-        "2.2" = cmc (range "8.16" "9.0") (range "2.0" "2.3");
-        "1.17" = cmc (range "8.10" "8.18") (range "1.12.0" "1.18.0");
-        "1.11" = cmc (range "8.10" "8.12") "1.11.0";
-      }
-    )) null;
+    with lib.versions;
+    lib.switch
+      [ coq.coq-version mathcomp.version ]
+      [
+        (case (range "8.16" "9.0") (range "2.0" "2.4") "2.3")
+        (case (range "8.16" "9.0") (range "2.0" "2.3") "2.2")
+        (case (range "8.10" "8.18") (range "1.12.0" "1.18.0") "1.17")
+        (case (range "8.10" "8.12") "1.11.0" "1.11")
+      ]
+      null;
 
   propagatedBuildInputs = [
     mathcomp.boot
diff --git a/pkgs/development/coq-modules/graph-theory/default.nix b/pkgs/development/coq-modules/graph-theory/default.nix
index ab4eb73fc7e9..57b89553b553 100644
--- a/pkgs/development/coq-modules/graph-theory/default.nix
+++ b/pkgs/development/coq-modules/graph-theory/default.nix
@@ -24,23 +24,27 @@ mkCoqDerivation {
 
   inherit version;
   defaultVersion =
-    with lib.versions;
     let
-      cmc = c: mc: [
-        c
-        mc
-      ];
+      case = coq: mc: out: {
+        case = [
+          coq
+          mc
+        ];
+        inherit out;
+      };
     in
-    lib.switch [ coq.coq-version mathcomp.version ] (lib.lists.sort (x: y: isLe x.out y.out) (
-      lib.mapAttrsToList (out: cases: { inherit cases out; }) {
-        "0.9.6" = cmc (range "8.18" "9.0") (range "2.0.0" "2.4.0");
-        "0.9.4" = cmc (range "8.16" "8.19") (range "2.0.0" "2.3.0");
-        "0.9.3" = cmc (range "8.16" "8.18") (range "2.0.0" "2.1.0");
-        "0.9.2" = cmc (range "8.14" "8.18") (range "1.13.0" "1.18.0");
-        "0.9.1" = cmc (range "8.14" "8.16") (range "1.13.0" "1.14.0");
-        "0.9" = cmc (range "8.12" "8.13") (range "1.12.0" "1.14.0");
-      }
-    )) null;
+    with lib.versions;
+    lib.switch
+      [ coq.coq-version mathcomp.version ]
+      [
+        (case (range "8.18" "9.0") (range "2.0.0" "2.4.0") "0.9.6")
+        (case (range "8.16" "8.19") (range "2.0.0" "2.3.0") "0.9.4")
+        (case (range "8.16" "8.18") (range "2.0.0" "2.1.0") "0.9.3")
+        (case (range "8.14" "8.18") (range "1.13.0" "1.18.0") "0.9.2")
+        (case (range "8.14" "8.16") (range "1.13.0" "1.14.0") "0.9.1")
+        (case (range "8.12" "8.13") (range "1.12.0" "1.14.0") "0.9")
+      ]
+      null;
 
   propagatedBuildInputs = [
     mathcomp.algebra
diff --git a/pkgs/development/coq-modules/hierarchy-builder/default.nix b/pkgs/development/coq-modules/hierarchy-builder/default.nix
index fc57e1b44834..cf37bf147d4c 100644
--- a/pkgs/development/coq-modules/hierarchy-builder/default.nix
+++ b/pkgs/development/coq-modules/hierarchy-builder/default.nix
@@ -14,20 +14,21 @@ let
     owner = "math-comp";
     inherit version;
     defaultVersion =
+      let
+        case = case: out: { inherit case out; };
+      in
       with lib.versions;
-      lib.switch coq.coq-version (lib.lists.sort (x: y: isLe x.out y.out) (
-        lib.mapAttrsToList (out: case: { inherit case out; }) {
-          "1.9.1" = range "8.20" "9.0";
-          "1.8.0" = range "8.19" "8.20";
-          "1.7.1" = range "8.18" "8.20";
-          "1.6.0" = range "8.16" "8.18";
-          "1.5.0" = range "8.15" "8.18";
-          "1.4.0" = range "8.15" "8.17";
-          "1.2.0" = range "8.13" "8.14";
-          "1.1.0" = range "8.12" "8.13";
-          "0.10.0" = isEq "8.11";
-        }
-      )) null;
+      lib.switch coq.coq-version [
+        (case (range "8.20" "9.0") "1.9.1")
+        (case (range "8.19" "8.20") "1.8.0")
+        (case (range "8.18" "8.20") "1.7.1")
+        (case (range "8.16" "8.18") "1.6.0")
+        (case (range "8.15" "8.18") "1.5.0")
+        (case (range "8.15" "8.17") "1.4.0")
+        (case (range "8.13" "8.14") "1.2.0")
+        (case (range "8.12" "8.13") "1.1.0")
+        (case (isEq "8.11") "0.10.0")
+      ] null;
     release."1.9.1".sha256 = "sha256-AiS0ezMyfIYlXnuNsVLz1GlKQZzJX+ilkrKkbo0GrF0=";
     release."1.8.1".sha256 = "sha256-Z0WAHDyycqgL+Le/zNfEAoLWzFb7WIL+3G3vEBExlb4=";
     release."1.8.0".sha256 = "sha256-4s/4ZZKj5tiTtSHGIM8Op/Pak4Vp52WVOpd4l9m19fY=";
diff --git a/pkgs/development/coq-modules/http/default.nix b/pkgs/development/coq-modules/http/default.nix
index 926f2b743712..9d35d8c6ca84 100644
--- a/pkgs/development/coq-modules/http/default.nix
+++ b/pkgs/development/coq-modules/http/default.nix
@@ -15,13 +15,12 @@ mkCoqDerivation {
 
   defaultVersion =
     let
-      inherit (lib.versions) isLe range;
+      case = case: out: { inherit case out; };
+      inherit (lib.versions) range;
     in
-    lib.switch coq.coq-version (lib.lists.sort (x: y: isLe x.out y.out) (
-      lib.mapAttrsToList (out: case: { inherit case out; }) {
-        "0.2.1" = range "8.14" "8.19";
-      }
-    )) null;
+    lib.switch coq.coq-version [
+      (case (range "8.14" "8.19") "0.2.1")
+    ] null;
   release = {
     "0.2.1".sha256 = "sha256-CIcaXEojNdajXNoMBjGlQRc1sOJSKgUlditNxbNSPgk=";
   };
diff --git a/pkgs/development/coq-modules/hydra-battles/default.nix b/pkgs/development/coq-modules/hydra-battles/default.nix
index 648a6d3229fc..985cfd2853bf 100644
--- a/pkgs/development/coq-modules/hydra-battles/default.nix
+++ b/pkgs/development/coq-modules/hydra-battles/default.nix
@@ -19,13 +19,14 @@
 
   inherit version;
   defaultVersion =
+    let
+      case = case: out: { inherit case out; };
+    in
     with lib.versions;
-    lib.switch coq.coq-version (lib.lists.sort (x: y: isLe x.out y.out) (
-      lib.mapAttrsToList (out: case: { inherit case out; }) {
-        "0.9" = range "8.13" "8.16";
-        "0.4" = range "8.11" "8.12";
-      }
-    )) null;
+    lib.switch coq.coq-version [
+      (case (range "8.13" "8.16") "0.9")
+      (case (range "8.11" "8.12") "0.4")
+    ] null;
 
   useDune = true;
 
diff --git a/pkgs/development/coq-modules/interval/default.nix b/pkgs/development/coq-modules/interval/default.nix
index eff13fb6b1f5..d46d4cf043c1 100644
--- a/pkgs/development/coq-modules/interval/default.nix
+++ b/pkgs/development/coq-modules/interval/default.nix
@@ -18,21 +18,22 @@ mkCoqDerivation rec {
   domain = "gitlab.inria.fr";
   inherit version;
   defaultVersion =
+    let
+      case = case: out: { inherit case out; };
+    in
     with lib.versions;
-    lib.switch coq.coq-version (lib.lists.sort (x: y: isLe x.out y.out) (
-      lib.mapAttrsToList (out: case: { inherit case out; }) {
-        "4.11.2" = range "8.13" "9.0";
-        "4.11.1" = range "8.13" "8.20";
-        "4.10.0" = range "8.12" "8.19";
-        "4.9.0" = range "8.12" "8.18";
-        "4.8.0" = range "8.12" "8.17";
-        "4.6.0" = range "8.12" "8.16";
-        "4.5.2" = range "8.8" "8.16";
-        "4.0.0" = range "8.8" "8.12";
-        "3.4.2" = range "8.7" "8.11";
-        "3.3.0" = range "8.5" "8.6";
-      }
-    )) null;
+    lib.switch coq.coq-version [
+      (case (range "8.13" "9.0") "4.11.2")
+      (case (range "8.13" "8.20") "4.11.1")
+      (case (range "8.12" "8.19") "4.10.0")
+      (case (range "8.12" "8.18") "4.9.0")
+      (case (range "8.12" "8.17") "4.8.0")
+      (case (range "8.12" "8.16") "4.6.0")
+      (case (range "8.8" "8.16") "4.5.2")
+      (case (range "8.8" "8.12") "4.0.0")
+      (case (range "8.7" "8.11") "3.4.2")
+      (case (range "8.5" "8.6") "3.3.0")
+    ] null;
   release."4.11.2".sha256 = "sha256-ouhjHtlxcqt06+Pt+UZAzwp83bVYPh3N+8jnsVvapSU=";
   release."4.11.1".sha256 = "sha256-QWZvU468rOhK796xCCEawW6rhCRTPnE0iLll9ynKflo=";
   release."4.11.0".sha256 = "sha256-vPwa4zSjyvxHLGDoNaBnHV2pb77dnQFbC50BL80fcvE=";
diff --git a/pkgs/development/coq-modules/iris/default.nix b/pkgs/development/coq-modules/iris/default.nix
index 7bfdd94d3c27..b58ea00f12da 100644
--- a/pkgs/development/coq-modules/iris/default.nix
+++ b/pkgs/development/coq-modules/iris/default.nix
@@ -12,18 +12,19 @@ mkCoqDerivation {
   owner = "iris";
   inherit version;
   defaultVersion =
+    let
+      case = case: out: { inherit case out; };
+    in
     with lib.versions;
-    lib.switch coq.coq-version (lib.lists.sort (x: y: isLe x.out y.out) (
-      lib.mapAttrsToList (out: case: { inherit case out; }) {
-        "4.3.0" = range "8.19" "9.0";
-        "4.2.0" = range "8.18" "8.19";
-        "4.1.0" = range "8.16" "8.18";
-        "4.0.0" = range "8.13" "8.17";
-        "3.5.0" = range "8.12" "8.14";
-        "3.4.0" = range "8.11" "8.13";
-        "3.3.0" = range "8.9" "8.10";
-      }
-    )) null;
+    lib.switch coq.coq-version [
+      (case (range "8.19" "9.0") "4.3.0")
+      (case (range "8.18" "8.19") "4.2.0")
+      (case (range "8.16" "8.18") "4.1.0")
+      (case (range "8.13" "8.17") "4.0.0")
+      (case (range "8.12" "8.14") "3.5.0")
+      (case (range "8.11" "8.13") "3.4.0")
+      (case (range "8.9" "8.10") "3.3.0")
+    ] null;
   release."4.3.0".sha256 = "sha256-3qhjiFI+A3I3fD8rFfJL5Hek77wScfn/FNNbDyGqA1k=";
   release."4.2.0".sha256 = "sha256-HuiHIe+5letgr1NN1biZZFq0qlWUbFmoVI7Q91+UIfM=";
   release."4.1.0".sha256 = "sha256-nTZUeZOXiH7HsfGbMKDE7vGrNVCkbMaWxdMWUcTUNlo=";
diff --git a/pkgs/development/coq-modules/itauto/default.nix b/pkgs/development/coq-modules/itauto/default.nix
index e7183563d8d4..690298742b9a 100644
--- a/pkgs/development/coq-modules/itauto/default.nix
+++ b/pkgs/development/coq-modules/itauto/default.nix
@@ -22,19 +22,20 @@
   release."8.13+no".sha256 = "sha256-gXoxtLcHPoyjJkt7WqvzfCMCQlh6kL2KtCGe3N6RC/A=";
   inherit version;
   defaultVersion =
+    let
+      case = case: out: { inherit case out; };
+    in
     with lib.versions;
-    lib.switch coq.coq-version (lib.lists.sort (x: y: isLe x.out y.out) (
-      lib.mapAttrsToList (out: case: { inherit case out; }) {
-        "8.20.0" = isEq "8.20";
-        "8.19.0" = isEq "8.19";
-        "8.18.0" = isEq "8.18";
-        "8.17.0" = isEq "8.17";
-        "8.16.0" = isEq "8.16";
-        "8.15.0" = isEq "8.15";
-        "8.14.0" = isEq "8.14";
-        "8.13+no" = isEq "8.13";
-      }
-    )) null;
+    lib.switch coq.coq-version [
+      (case (isEq "8.20") "8.20.0")
+      (case (isEq "8.19") "8.19.0")
+      (case (isEq "8.18") "8.18.0")
+      (case (isEq "8.17") "8.17.0")
+      (case (isEq "8.16") "8.16.0")
+      (case (isEq "8.15") "8.15.0")
+      (case (isEq "8.14") "8.14.0")
+      (case (isEq "8.13") "8.13+no")
+    ] null;
 
   mlPlugin = true;
   nativeBuildInputs = (with coq.ocamlPackages; [ ocamlbuild ]);
diff --git a/pkgs/development/coq-modules/itree-io/default.nix b/pkgs/development/coq-modules/itree-io/default.nix
index c3df0dbf49a1..1b5624cf5bc9 100644
--- a/pkgs/development/coq-modules/itree-io/default.nix
+++ b/pkgs/development/coq-modules/itree-io/default.nix
@@ -15,13 +15,12 @@ mkCoqDerivation {
 
   defaultVersion =
     let
-      inherit (lib.versions) isLe range;
+      case = case: out: { inherit case out; };
+      inherit (lib.versions) range;
     in
-    lib.switch coq.coq-version (lib.lists.sort (x: y: isLe x.out y.out) (
-      lib.mapAttrsToList (out: case: { inherit case out; }) {
-        "0.1.1" = range "8.12" "8.19";
-      }
-    )) null;
+    lib.switch coq.coq-version [
+      (case (range "8.12" "8.19") "0.1.1")
+    ] null;
   release = {
     "0.1.1".sha256 = "sha256-IFwIj8dxW4jm2gvuUJ8LKZFSJeljp0bsn8fezxY6t2o=";
   };
diff --git a/pkgs/development/coq-modules/jasmin/default.nix b/pkgs/development/coq-modules/jasmin/default.nix
index c53ab153f3e9..c58cba094a18 100644
--- a/pkgs/development/coq-modules/jasmin/default.nix
+++ b/pkgs/development/coq-modules/jasmin/default.nix
@@ -14,19 +14,23 @@ mkCoqDerivation {
 
   inherit version;
   defaultVersion =
-    with lib.versions;
     let
-      cmc = c: mc: [
-        c
-        mc
-      ];
+      case = coq: mc: out: {
+        case = [
+          coq
+          mc
+        ];
+        inherit out;
+      };
     in
-    lib.switch [ coq.coq-version mathcomp.version ] (lib.lists.sort (x: y: isLe x.out y.out) (
-      lib.mapAttrsToList (out: cases: { inherit cases out; }) {
-        "2025.02.0" = cmc (range "8.19" "9.0") (range "2.2" "2.4");
-        "2024.07.2" = cmc (isEq "8.18") (isEq "2.2");
-      }
-    )) null;
+    with lib.versions;
+    lib.switch
+      [ coq.coq-version mathcomp.version ]
+      [
+        (case (range "8.19" "9.0") (range "2.2" "2.4") "2025.02.0")
+        (case (isEq "8.18") (isEq "2.2") "2024.07.2")
+      ]
+      null;
   releaseRev = v: "v${v}";
 
   release."2025.02.0".sha256 = "sha256-Jlf0+VPuYWXdWyKHKHSp7h/HuCCp4VkcrgDAmh7pi5s=";
diff --git a/pkgs/development/coq-modules/json/default.nix b/pkgs/development/coq-modules/json/default.nix
index b48b8de4ec89..06f18199fcf1 100644
--- a/pkgs/development/coq-modules/json/default.nix
+++ b/pkgs/development/coq-modules/json/default.nix
@@ -15,14 +15,13 @@
 
   defaultVersion =
     let
-      inherit (lib.versions) isLe range;
+      case = case: out: { inherit case out; };
+      inherit (lib.versions) range;
     in
-    lib.switch coq.coq-version (lib.lists.sort (x: y: isLe x.out y.out) (
-      lib.mapAttrsToList (out: case: { inherit case out; }) {
-        "0.2.0" = range "8.14" "9.0";
-        "0.1.3" = range "8.14" "8.20";
-      }
-    )) null;
+    lib.switch coq.coq-version [
+      (case (range "8.14" "9.0") "0.2.0")
+      (case (range "8.14" "8.20") "0.1.3")
+    ] null;
   release = {
     "0.2.0".sha256 = "sha256-qDRTgWLUvu4x3/d3BDcqo2I4W5ZmLyRiwuY/Tm/FuKA=";
     "0.1.3".sha256 = "sha256-lElAzW4IuX+BB6ngDjlyKn0MytLRfbhQanB+Lct/WR0=";
diff --git a/pkgs/development/coq-modules/mathcomp-abel/default.nix b/pkgs/development/coq-modules/mathcomp-abel/default.nix
index 925cbbdc62a7..9fb880f99c8f 100644
--- a/pkgs/development/coq-modules/mathcomp-abel/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-abel/default.nix
@@ -18,20 +18,24 @@ mkCoqDerivation {
 
   inherit version;
   defaultVersion =
-    with lib.versions;
     let
-      cmc = c: mc: [
-        c
-        mc
-      ];
+      case = coq: mc: out: {
+        case = [
+          coq
+          mc
+        ];
+        inherit out;
+      };
     in
-    lib.switch [ coq.coq-version mathcomp.version ] (lib.lists.sort (x: y: isLe x.out y.out) (
-      lib.mapAttrsToList (out: cases: { inherit cases out; }) {
-        "1.2.1" = cmc (range "8.10" "8.16") (range "1.12.0" "1.15.0");
-        "1.2.0" = cmc (range "8.10" "8.15") (range "1.12.0" "1.14.0");
-        "1.1.2" = cmc (range "8.10" "8.14") (range "1.11.0" "1.12.0");
-      }
-    )) null;
+    with lib.versions;
+    lib.switch
+      [ coq.coq-version mathcomp.version ]
+      [
+        (case (range "8.10" "8.16") (range "1.12.0" "1.15.0") "1.2.1")
+        (case (range "8.10" "8.15") (range "1.12.0" "1.14.0") "1.2.0")
+        (case (range "8.10" "8.14") (range "1.11.0" "1.12.0") "1.1.2")
+      ]
+      null;
 
   release."1.2.1".sha256 = "sha256-M1q6WIPBsayHde2hwlTxylH169hcTs3OuFsEkM0e3yc=";
   release."1.2.0".sha256 = "1picd4m85ipj22j3b84cv8ab3330radzrhd6kp0gpxq14dhv02c2";
diff --git a/pkgs/development/coq-modules/mathcomp-algebra-tactics/default.nix b/pkgs/development/coq-modules/mathcomp-algebra-tactics/default.nix
index fc4cca84b4d0..8f1b2ab26d48 100644
--- a/pkgs/development/coq-modules/mathcomp-algebra-tactics/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-algebra-tactics/default.nix
@@ -19,22 +19,26 @@ mkCoqDerivation {
   inherit version;
 
   defaultVersion =
-    with lib.versions;
     let
-      cmc = c: mc: [
-        c
-        mc
-      ];
+      case = coq: mc: out: {
+        case = [
+          coq
+          mc
+        ];
+        inherit out;
+      };
     in
-    lib.switch [ coq.coq-version mathcomp-algebra.version ] (lib.lists.sort (x: y: isLe x.out y.out) (
-      lib.mapAttrsToList (out: cases: { inherit cases out; }) {
-        "1.2.5" = cmc (range "8.20" "9.0") (isGe "2.4");
-        "1.2.4" = cmc (range "8.16" "9.0") (isGe "2.0");
-        "1.2.2" = cmc (range "8.16" "8.18") (isGe "2.0");
-        "1.1.1" = cmc (range "8.16" "8.19") (isGe "1.15");
-        "1.0.0" = cmc (range "8.13" "8.16") (isGe "1.12");
-      }
-    )) null;
+    with lib.versions;
+    lib.switch
+      [ coq.coq-version mathcomp-algebra.version ]
+      [
+        (case (range "8.20" "9.0") (isGe "2.4") "1.2.5")
+        (case (range "8.16" "9.0") (isGe "2.0") "1.2.4")
+        (case (range "8.16" "8.18") (isGe "2.0") "1.2.2")
+        (case (range "8.16" "8.19") (isGe "1.15") "1.1.1")
+        (case (range "8.13" "8.16") (isGe "1.12") "1.0.0")
+      ]
+      null;
 
   release."1.0.0".sha256 = "sha256-kszARPBizWbxSQ/Iqpf2vLbxYc6AjpUCLnSNlPcNfls=";
   release."1.1.1".sha256 = "sha256-5wItMeeTRoJlRBH3zBNc2VUZn6pkDde60YAvXTx+J3U=";
diff --git a/pkgs/development/coq-modules/mathcomp-analysis/default.nix b/pkgs/development/coq-modules/mathcomp-analysis/default.nix
index b24c6fa18849..f87d9ed34893 100644
--- a/pkgs/development/coq-modules/mathcomp-analysis/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-analysis/default.nix
@@ -44,32 +44,36 @@ let
   release."0.2.3".sha256 = "0p9mr8g1qma6h10qf7014dv98ln90dfkwn76ynagpww7qap8s966";
 
   defaultVersion =
-    with lib.versions;
     let
-      cmc = c: mc: [
-        c
-        mc
-      ];
+      case = coq: mc: out: {
+        case = [
+          coq
+          mc
+        ];
+        inherit out;
+      };
     in
-    lib.switch [ coq.coq-version mathcomp.version ] (lib.lists.sort (x: y: isLe x.out y.out) (
-      lib.mapAttrsToList (out: cases: { inherit cases out; }) {
-        "1.11.0" = cmc (range "8.20" "9.0") (range "2.1.0" "2.4.0");
-        "1.9.0" = cmc (range "8.19" "8.20") (range "2.1.0" "2.3.0");
-        "1.1.0" = cmc (range "8.17" "8.20") (range "2.0.0" "2.2.0");
-        "0.7.0" = cmc (range "8.17" "8.19") (range "1.17.0" "1.19.0");
-        "0.6.7" = cmc (range "8.17" "8.18") (range "1.15.0" "1.18.0");
-        "0.6.6" = cmc (range "8.17" "8.18") (range "1.15.0" "1.18.0");
-        "0.6.5" = cmc (range "8.14" "8.18") (range "1.15.0" "1.17.0");
-        "0.6.1" = cmc (range "8.14" "8.18") (range "1.13.0" "1.16.0");
-        "0.5.2" = cmc (range "8.14" "8.18") (range "1.13" "1.15");
-        "0.5.1" = cmc (range "8.13" "8.15") (range "1.13" "1.14");
-        "0.3.13" = cmc (range "8.13" "8.15") (range "1.12" "1.14");
-        "0.3.10" = cmc (range "8.11" "8.14") (range "1.12" "1.13");
-        "0.3.3" = cmc (range "8.10" "8.12") "1.11.0";
-        "0.3.1" = cmc (range "8.10" "8.11") "1.11.0";
-        "0.2.3" = cmc (range "8.8" "8.11") (range "1.8" "1.10");
-      }
-    )) null;
+    with lib.versions;
+    lib.switch
+      [ coq.coq-version mathcomp.version ]
+      [
+        (case (range "8.20" "9.0") (range "2.1.0" "2.4.0") "1.11.0")
+        (case (range "8.19" "8.20") (range "2.1.0" "2.3.0") "1.9.0")
+        (case (range "8.17" "8.20") (range "2.0.0" "2.2.0") "1.1.0")
+        (case (range "8.17" "8.19") (range "1.17.0" "1.19.0") "0.7.0")
+        (case (range "8.17" "8.18") (range "1.15.0" "1.18.0") "0.6.7")
+        (case (range "8.17" "8.18") (range "1.15.0" "1.18.0") "0.6.6")
+        (case (range "8.14" "8.18") (range "1.15.0" "1.17.0") "0.6.5")
+        (case (range "8.14" "8.18") (range "1.13.0" "1.16.0") "0.6.1")
+        (case (range "8.14" "8.18") (range "1.13" "1.15") "0.5.2")
+        (case (range "8.13" "8.15") (range "1.13" "1.14") "0.5.1")
+        (case (range "8.13" "8.15") (range "1.12" "1.14") "0.3.13")
+        (case (range "8.11" "8.14") (range "1.12" "1.13") "0.3.10")
+        (case (range "8.10" "8.12") "1.11.0" "0.3.3")
+        (case (range "8.10" "8.11") "1.11.0" "0.3.1")
+        (case (range "8.8" "8.11") (range "1.8" "1.10") "0.2.3")
+      ]
+      null;
 
   # list of analysis packages sorted by dependency order
   packages = {
diff --git a/pkgs/development/coq-modules/mathcomp-apery/default.nix b/pkgs/development/coq-modules/mathcomp-apery/default.nix
index 697d0e970e6a..45501f1969a0 100644
--- a/pkgs/development/coq-modules/mathcomp-apery/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-apery/default.nix
@@ -17,18 +17,22 @@ mkCoqDerivation {
 
   inherit version;
   defaultVersion =
-    with lib.versions;
     let
-      cmc = c: mc: [
-        c
-        mc
-      ];
+      case = coq: mc: out: {
+        case = [
+          coq
+          mc
+        ];
+        inherit out;
+      };
     in
-    lib.switch [ coq.coq-version mathcomp.version ] (lib.lists.sort (x: y: isLe x.out y.out) (
-      lib.mapAttrsToList (out: cases: { inherit cases out; }) {
-        "1.0.2" = cmc (range "8.13" "8.16") (range "1.12.0" "1.17.0");
-      }
-    )) null;
+    with lib.versions;
+    lib.switch
+      [ coq.coq-version mathcomp.version ]
+      [
+        (case (range "8.13" "8.16") (range "1.12.0" "1.17.0") "1.0.2")
+      ]
+      null;
 
   release."1.0.2".sha256 = "sha256-llxyMKYvWUA7fyroG1S/jtpioAoArmarR1edi3cikcY=";
 
diff --git a/pkgs/development/coq-modules/mathcomp-bigenough/default.nix b/pkgs/development/coq-modules/mathcomp-bigenough/default.nix
index 357fd97d93cf..8e50d9a4ea86 100644
--- a/pkgs/development/coq-modules/mathcomp-bigenough/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-bigenough/default.nix
@@ -22,13 +22,14 @@ mkCoqDerivation {
   };
   inherit version;
   defaultVersion =
+    let
+      case = case: out: { inherit case out; };
+    in
     with lib.versions;
-    lib.switch coq.coq-version (lib.lists.sort (x: y: isLe x.out y.out) (
-      lib.mapAttrsToList (out: case: { inherit case out; }) {
-        "1.0.2" = range "8.10" "9.0";
-        "1.0.0" = range "8.5" "8.14";
-      }
-    )) null;
+    lib.switch coq.coq-version [
+      (case (range "8.10" "9.0") "1.0.2")
+      (case (range "8.5" "8.14") "1.0.0")
+    ] null;
 
   propagatedBuildInputs = [ mathcomp-boot ];
 
diff --git a/pkgs/development/coq-modules/mathcomp-finmap/default.nix b/pkgs/development/coq-modules/mathcomp-finmap/default.nix
index 97dd95556200..82c1bf7ac48f 100644
--- a/pkgs/development/coq-modules/mathcomp-finmap/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-finmap/default.nix
@@ -16,28 +16,32 @@ mkCoqDerivation {
   owner = "math-comp";
   inherit version;
   defaultVersion =
-    with lib.versions;
     let
-      cmc = c: mc: [
-        c
-        mc
-      ];
+      case = coq: mc: out: {
+        case = [
+          coq
+          mc
+        ];
+        inherit out;
+      };
     in
-    lib.switch [ coq.coq-version mathcomp-boot.version ] (lib.lists.sort (x: y: isLe x.out y.out) (
-      lib.mapAttrsToList (out: cases: { inherit cases out; }) {
-        "2.2.0" = cmc (range "8.20" "9.0") (range "2.3" "2.4");
-        "2.1.0" = cmc (range "8.16" "9.0") (range "2.0" "2.3");
-        "2.0.0" = cmc (range "8.16" "8.18") (range "2.0" "2.1");
-        "1.5.2" = cmc (range "8.13" "8.20") (range "1.12" "1.19");
-        "1.5.1" = cmc (isGe "8.10") (range "1.11" "1.17");
-        "1.5.0" = cmc (range "8.7" "8.11") "1.11.0";
-        "1.4.0+coq-8.11" = cmc (isEq "8.11") (range "1.8" "1.10");
-        "1.4.0" = cmc (range "8.7" "8.11.0") (range "1.8" "1.10");
-        "1.3.4" = cmc (range "8.7" "8.11.0") (range "1.8" "1.10");
-        "1.1.0" = cmc (range "8.7" "8.9") "1.7.0";
-        "1.0.0" = cmc (range "8.6" "8.7") (range "1.6.1" "1.7");
-      }
-    )) null;
+    with lib.versions;
+    lib.switch
+      [ coq.coq-version mathcomp-boot.version ]
+      [
+        (case (range "8.20" "9.0") (range "2.3" "2.4") "2.2.0")
+        (case (range "8.16" "9.0") (range "2.0" "2.3") "2.1.0")
+        (case (range "8.16" "8.18") (range "2.0" "2.1") "2.0.0")
+        (case (range "8.13" "8.20") (range "1.12" "1.19") "1.5.2")
+        (case (isGe "8.10") (range "1.11" "1.17") "1.5.1")
+        (case (range "8.7" "8.11") "1.11.0" "1.5.0")
+        (case (isEq "8.11") (range "1.8" "1.10") "1.4.0+coq-8.11")
+        (case (range "8.7" "8.11.0") (range "1.8" "1.10") "1.4.0")
+        (case (range "8.7" "8.11.0") (range "1.8" "1.10") "1.3.4")
+        (case (range "8.7" "8.9") "1.7.0" "1.1.0")
+        (case (range "8.6" "8.7") (range "1.6.1" "1.7") "1.0.0")
+      ]
+      null;
   release = {
     "2.2.0".sha256 = "sha256-oDQEZOutrJxmN8FvzovUIhqw0mwc8Ej7thrieJrW8BY=";
     "2.1.0".sha256 = "sha256-gh0cnhdVDyo+D5zdtxLc10kGKQLQ3ITzHnMC45mCtpY=";
diff --git a/pkgs/development/coq-modules/mathcomp-infotheo/default.nix b/pkgs/development/coq-modules/mathcomp-infotheo/default.nix
index 25d3827a89e3..6a29a390174a 100644
--- a/pkgs/development/coq-modules/mathcomp-infotheo/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-infotheo/default.nix
@@ -19,27 +19,31 @@
   inherit version;
 
   defaultVersion =
-    with lib.versions;
     let
-      cmc = c: mc: [
-        c
-        mc
-      ];
+      case = coq: mc: out: {
+        case = [
+          coq
+          mc
+        ];
+        inherit out;
+      };
     in
-    lib.switch [ coq.coq-version mathcomp-analysis.version ] (lib.lists.sort (x: y: isLe x.out y.out) (
-      lib.mapAttrsToList (out: cases: { inherit cases out; }) {
-        "0.9.3" = cmc (range "8.20" "8.20") (isGe "1.10");
-        "0.9.1" = cmc (range "8.19" "8.20") (isGe "1.9");
-        "0.7.7" = cmc (range "8.19" "8.20") (isGe "1.7");
-        "0.7.5" = cmc (range "8.19" "8.20") (isGe "1.7");
-        "0.7.3" = cmc (range "8.18" "8.20") (isGe "1.5");
-        "0.7.2" = cmc (range "8.18" "8.19") (isGe "1.2");
-        "0.7.1" = cmc (range "8.17" "8.19") (isGe "1.0");
-        "0.6.1" = cmc (isGe "8.17") (range "0.6.6" "0.7.0");
-        "0.5.2" = cmc (range "8.17" "8.18") (range "0.6.0" "0.6.7");
-        "0.5.1" = cmc (range "8.15" "8.16") (range "0.5.4" "0.6.5");
-      }
-    )) null;
+    with lib.versions;
+    lib.switch
+      [ coq.coq-version mathcomp-analysis.version ]
+      [
+        (case (range "8.20" "8.20") (isGe "1.10") "0.9.3")
+        (case (range "8.19" "8.20") (isGe "1.9") "0.9.1")
+        (case (range "8.19" "8.20") (isGe "1.7") "0.7.7")
+        (case (range "8.19" "8.20") (isGe "1.7") "0.7.5")
+        (case (range "8.18" "8.20") (isGe "1.5") "0.7.3")
+        (case (range "8.18" "8.19") (isGe "1.2") "0.7.2")
+        (case (range "8.17" "8.19") (isGe "1.0") "0.7.1")
+        (case (isGe "8.17") (range "0.6.6" "0.7.0") "0.6.1")
+        (case (range "8.17" "8.18") (range "0.6.0" "0.6.7") "0.5.2")
+        (case (range "8.15" "8.16") (range "0.5.4" "0.6.5") "0.5.1")
+      ]
+      null;
   release."0.9.3".sha256 = "sha256-8+cnVKNAvZ3MVV3BpS8UmCIxJphsQRBv3swek1eEBjE=";
   release."0.9.1".sha256 = "sha256-WI20HxMHr1ZUwOGPIUl+nRI8TxVUa2+F1xcGjRDHO9g=";
   release."0.7.7".sha256 = "sha256-kEbpMl7U+I2kvqi1VrjhIVFkZFO6h0tTHEUZRbHYG7E=";
diff --git a/pkgs/development/coq-modules/mathcomp-tarjan/default.nix b/pkgs/development/coq-modules/mathcomp-tarjan/default.nix
index a8d233af7d3b..383da1bd8231 100644
--- a/pkgs/development/coq-modules/mathcomp-tarjan/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-tarjan/default.nix
@@ -18,21 +18,25 @@ mkCoqDerivation {
 
   inherit version;
   defaultVersion =
-    with lib.versions;
     let
-      cmc = c: mc: [
-        c
-        mc
-      ];
+      case = coq: mc: out: {
+        case = [
+          coq
+          mc
+        ];
+        inherit out;
+      };
     in
-    lib.switch [ coq.coq-version mathcomp-ssreflect.version ] (lib.lists.sort (x: y: isLe x.out y.out) (
-      lib.mapAttrsToList (out: cases: { inherit cases out; }) {
-        "1.0.3" = cmc (range "8.16" "9.0") (range "2.0.0" "2.4.0");
-        "1.0.2" = cmc (range "8.16" "9.0") (range "2.0.0" "2.3.0");
-        "1.0.1" = cmc (range "8.12" "8.18") (range "1.12.0" "1.17.0");
-        "1.0.0" = cmc (range "8.10" "8.16") (range "1.12.0" "1.17.0");
-      }
-    )) null;
+    with lib.versions;
+    lib.switch
+      [ coq.coq-version mathcomp-ssreflect.version ]
+      [
+        (case (range "8.16" "9.0") (range "2.0.0" "2.4.0") "1.0.3")
+        (case (range "8.16" "9.0") (range "2.0.0" "2.3.0") "1.0.2")
+        (case (range "8.12" "8.18") (range "1.12.0" "1.17.0") "1.0.1")
+        (case (range "8.10" "8.16") (range "1.12.0" "1.17.0") "1.0.0")
+      ]
+      null;
   release."1.0.3".sha256 = "sha256-5lpOCDyH6NFzGLvnXHHAnR7Qv5oXsUyC8TLBFrIiBag=";
   release."1.0.2".sha256 = "sha256-U20xgA+e9KTRdvILD1cxN6ia+dlA8uBTIbc4QlKz9ss=";
   release."1.0.1".sha256 = "sha256-utNjFCAqC5xOuhdyKhfMZkRYJD0xv9Gt6U3ZdQ56mek=";
diff --git a/pkgs/development/coq-modules/mathcomp-word/default.nix b/pkgs/development/coq-modules/mathcomp-word/default.nix
index c43d7a34f2f6..555b572c467b 100644
--- a/pkgs/development/coq-modules/mathcomp-word/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-word/default.nix
@@ -56,19 +56,23 @@ mkCoqDerivation {
 
   inherit version;
   defaultVersion =
-    with lib.versions;
     let
-      cmc = c: mc: [
-        c
-        mc
-      ];
+      case = coq: mc: out: {
+        case = [
+          coq
+          mc
+        ];
+        inherit out;
+      };
     in
-    lib.switch [ coq.coq-version mathcomp.version ] (lib.lists.sort (x: y: isLe x.out y.out) (
-      lib.mapAttrsToList (out: cases: { inherit cases out; }) {
-        "3.2" = cmc (range "8.16" "9.0") (isGe "2.0");
-        "2.4" = cmc (range "8.12" "8.20") (range "1.12" "1.19");
-      }
-    )) null;
+    with lib.versions;
+    lib.switch
+      [ coq.coq-version mathcomp.version ]
+      [
+        (case (range "8.16" "9.0") (isGe "2.0") "3.2")
+        (case (range "8.12" "8.20") (range "1.12" "1.19") "2.4")
+      ]
+      null;
 
   propagatedBuildInputs = [
     mathcomp.algebra
diff --git a/pkgs/development/coq-modules/mathcomp-zify/default.nix b/pkgs/development/coq-modules/mathcomp-zify/default.nix
index 2c91a5056496..8e4dd232dcff 100644
--- a/pkgs/development/coq-modules/mathcomp-zify/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-zify/default.nix
@@ -20,20 +20,24 @@ mkCoqDerivation {
   inherit version;
 
   defaultVersion =
-    with lib.versions;
     let
-      cmc = c: mc: [
-        c
-        mc
-      ];
+      case = coq: mc: out: {
+        case = [
+          coq
+          mc
+        ];
+        inherit out;
+      };
     in
-    lib.switch [ coq.coq-version mathcomp-algebra.version ] (lib.lists.sort (x: y: isLe x.out y.out) (
-      lib.mapAttrsToList (out: cases: { inherit cases out; }) {
-        "1.5.0+2.0+8.16" = cmc (range "8.16" "9.0") (isGe "2.0.0");
-        "1.3.0+1.12+8.13" = cmc (range "8.13" "8.20") (range "1.12" "1.19.0");
-        "1.1.0+1.12+8.13" = cmc (range "8.13" "8.16") (range "1.12" "1.17.0");
-      }
-    )) null;
+    with lib.versions;
+    lib.switch
+      [ coq.coq-version mathcomp-algebra.version ]
+      [
+        (case (range "8.16" "9.0") (isGe "2.0.0") "1.5.0+2.0+8.16")
+        (case (range "8.13" "8.20") (range "1.12" "1.19.0") "1.3.0+1.12+8.13")
+        (case (range "8.13" "8.16") (range "1.12" "1.17.0") "1.1.0+1.12+8.13")
+      ]
+      null;
 
   release."1.0.0+1.12+8.13".sha256 = "1j533vx6lacr89bj1bf15l1a0s7rvrx4l00wyjv99aczkfbz6h6k";
   release."1.1.0+1.12+8.13".sha256 = "1plf4v6q5j7wvmd5gsqlpiy0vwlw6hy5daq2x42gqny23w9mi2pr";
diff --git a/pkgs/development/coq-modules/mathcomp/default.nix b/pkgs/development/coq-modules/mathcomp/default.nix
index 0311a33a406c..f988a6284376 100644
--- a/pkgs/development/coq-modules/mathcomp/default.nix
+++ b/pkgs/development/coq-modules/mathcomp/default.nix
@@ -31,31 +31,30 @@ let
   withDoc = single && (args.withDoc or false);
   defaultVersion =
     let
-      inherit (lib.versions) isLe range;
+      case = case: out: { inherit case out; };
+      inherit (lib.versions) range;
     in
-    lib.switch coq.coq-version (lib.lists.sort (x: y: isLe x.out y.out) (
-      lib.mapAttrsToList (out: case: { inherit case out; }) {
-        "2.4.0" = range "8.20" "9.0";
-        "2.3.0" = range "8.19" "9.0";
-        "2.2.0" = range "8.17" "8.20";
-        "2.1.0" = range "8.17" "8.18";
-        "2.0.0" = range "8.17" "8.18";
-        "1.19.0" = range "8.19" "8.20";
-        "1.18.0" = range "8.17" "8.18";
-        "1.17.0" = range "8.15" "8.18";
-        "1.16.0" = range "8.13" "8.18";
-        "1.15.0" = range "8.14" "8.16";
-        "1.14.0" = range "8.11" "8.15";
-        "1.13.0" = range "8.11" "8.15";
-        "1.12.0" = range "8.10" "8.13";
-        "1.11.0" = range "8.7" "8.12";
-        "1.10.0" = range "8.7" "8.11";
-        "1.9.0" = range "8.7" "8.11";
-        "1.8.0" = range "8.7" "8.9";
-        "1.7.0" = range "8.6" "8.9";
-        "1.6.4" = range "8.5" "8.7";
-      }
-    )) null;
+    lib.switch coq.coq-version [
+      (case (range "8.20" "9.0") "2.4.0")
+      (case (range "8.19" "9.0") "2.3.0")
+      (case (range "8.17" "8.20") "2.2.0")
+      (case (range "8.17" "8.18") "2.1.0")
+      (case (range "8.17" "8.18") "2.0.0")
+      (case (range "8.19" "8.20") "1.19.0")
+      (case (range "8.17" "8.18") "1.18.0")
+      (case (range "8.15" "8.18") "1.17.0")
+      (case (range "8.13" "8.18") "1.16.0")
+      (case (range "8.14" "8.16") "1.15.0")
+      (case (range "8.11" "8.15") "1.14.0")
+      (case (range "8.11" "8.15") "1.13.0")
+      (case (range "8.10" "8.13") "1.12.0")
+      (case (range "8.7" "8.12") "1.11.0")
+      (case (range "8.7" "8.11") "1.10.0")
+      (case (range "8.7" "8.11") "1.9.0")
+      (case (range "8.7" "8.9") "1.8.0")
+      (case (range "8.6" "8.9") "1.7.0")
+      (case (range "8.5" "8.7") "1.6.4")
+    ] null;
   release = {
     "2.4.0".sha256 = "sha256-A1XgLLwZRvKS8QyceCkSQa7ue6TYyf5fMft5gSx9NOs=";
     "2.3.0".sha256 = "sha256-wa6OBig8rhAT4iwupSylyCAMhO69rADa0MQIX5zzL+Q=";
diff --git a/pkgs/development/coq-modules/metacoq/default.nix b/pkgs/development/coq-modules/metacoq/default.nix
index 2856547930ad..bb78843c736f 100644
--- a/pkgs/development/coq-modules/metacoq/default.nix
+++ b/pkgs/development/coq-modules/metacoq/default.nix
@@ -10,22 +10,24 @@
 let
   repo = "metacoq";
   owner = "MetaCoq";
-  defaultVersion = lib.switch coq.coq-version (lib.lists.sort (x: y: lib.versions.isLe x.out y.out) (
-    lib.mapAttrsToList (out: case: { inherit case out; }) {
-      "1.0-beta2-8.11" = "8.11";
-      "1.0-beta2-8.12" = "8.12";
+  defaultVersion =
+    let
+      case = case: out: { inherit case out; };
+    in
+    lib.switch coq.coq-version [
+      (case "8.11" "1.0-beta2-8.11")
+      (case "8.12" "1.0-beta2-8.12")
       # Do not provide 8.13 because it does not compile with equations 1.3 provided by default (only 1.2.3)
-      # "1.0-beta2-8.13" = "8.13";
-      "1.1-8.14" = "8.14";
-      "1.1-8.15" = "8.15";
-      "1.1-8.16" = "8.16";
-      "1.3.1-8.17" = "8.17";
-      "1.3.1-8.18" = "8.18";
-      "1.3.3-8.19" = "8.19";
-      "1.3.4-8.20" = "8.20";
-      "1.3.4-9.0" = "9.0";
-    }
-  )) null;
+      # (case "8.13" "1.0-beta2-8.13")
+      (case "8.14" "1.1-8.14")
+      (case "8.15" "1.1-8.15")
+      (case "8.16" "1.1-8.16")
+      (case "8.17" "1.3.1-8.17")
+      (case "8.18" "1.3.1-8.18")
+      (case "8.19" "1.3.3-8.19")
+      (case "8.20" "1.3.4-8.20")
+      (case "9.0" "1.3.4-9.0")
+    ] null;
   release = {
     "1.0-beta2-8.11".sha256 = "sha256-I9YNk5Di6Udvq5/xpLSNflfjRyRH8fMnRzbo3uhpXNs=";
     "1.0-beta2-8.12".sha256 = "sha256-I8gpmU9rUQJh0qfp5KOgDNscVvCybm5zX4TINxO1TVA=";
diff --git a/pkgs/development/coq-modules/metarocq/default.nix b/pkgs/development/coq-modules/metarocq/default.nix
index a90df150f409..aa7b39918427 100644
--- a/pkgs/development/coq-modules/metarocq/default.nix
+++ b/pkgs/development/coq-modules/metarocq/default.nix
@@ -10,11 +10,13 @@
 let
   repo = "metarocq";
   owner = "MetaRocq";
-  defaultVersion = lib.switch coq.coq-version (lib.lists.sort (x: y: lib.versions.isLe x.out y.out) (
-    lib.mapAttrsToList (out: case: { inherit case out; }) {
-      "1.4-9.0" = "9.0";
-    }
-  )) null;
+  defaultVersion =
+    let
+      case = case: out: { inherit case out; };
+    in
+    lib.switch coq.coq-version [
+      (case ("9.0") "1.4-9.0")
+    ] null;
   release = {
     "1.4-9.0".sha256 = "sha256-5QecDAMkvgfDPZ7/jDfnOgcE+Eb1LTAozP7nz6nkuxg=";
   };
diff --git a/pkgs/development/coq-modules/multinomials/default.nix b/pkgs/development/coq-modules/multinomials/default.nix
index 6cb2adc7aba6..8b2f7608afc8 100644
--- a/pkgs/development/coq-modules/multinomials/default.nix
+++ b/pkgs/development/coq-modules/multinomials/default.nix
@@ -20,30 +20,34 @@ mkCoqDerivation {
 
   inherit version;
   defaultVersion =
-    with lib.versions;
     let
-      cmc = c: mc: [
-        c
-        mc
-      ];
+      case = coq: mc: out: {
+        case = [
+          coq
+          mc
+        ];
+        inherit out;
+      };
     in
-    lib.switch [ coq.coq-version mathcomp.version ] (lib.lists.sort (x: y: isLe x.out y.out) (
-      lib.mapAttrsToList (out: cases: { inherit cases out; }) {
-        "2.4.0" = cmc (range "8.18" "9.0") (range "2.1.0" "2.4.0");
-        "2.3.0" = cmc (range "8.17" "9.0") (range "2.1.0" "2.3.0");
-        "2.2.0" = cmc (range "8.17" "8.20") (isGe "2.1.0");
-        "2.1.0" = cmc (range "8.16" "8.18") "2.1.0";
-        "2.0.0" = cmc (range "8.16" "8.18") "2.0.0";
-        "1.6.0" = cmc (isGe "8.15") (range "1.15.0" "1.19.0");
-        "1.5.6" = cmc (isGe "8.10") (range "1.13.0" "1.17.0");
-        "1.5.5" = cmc (range "8.10" "8.16") (range "1.12.0" "1.15.0");
-        "1.5.3" = cmc (range "8.10" "8.12") "1.12.0";
-        "1.5.2" = cmc (range "8.7" "8.12") "1.11.0";
-        "1.5.0" = cmc (range "8.7" "8.11") (range "1.8" "1.10");
-        "1.4" = cmc (range "8.7" "8.10") (range "1.8" "1.10");
-        "1.1" = cmc "8.6" (range "1.6" "1.7");
-      }
-    )) null;
+    with lib.versions;
+    lib.switch
+      [ coq.coq-version mathcomp.version ]
+      [
+        (case (range "8.18" "9.0") (range "2.1.0" "2.4.0") "2.4.0")
+        (case (range "8.17" "9.0") (range "2.1.0" "2.3.0") "2.3.0")
+        (case (range "8.17" "8.20") (isGe "2.1.0") "2.2.0")
+        (case (range "8.16" "8.18") "2.1.0" "2.1.0")
+        (case (range "8.16" "8.18") "2.0.0" "2.0.0")
+        (case (isGe "8.15") (range "1.15.0" "1.19.0") "1.6.0")
+        (case (isGe "8.10") (range "1.13.0" "1.17.0") "1.5.6")
+        (case (range "8.10" "8.16") (range "1.12.0" "1.15.0") "1.5.5")
+        (case (range "8.10" "8.12") "1.12.0" "1.5.3")
+        (case (range "8.7" "8.12") "1.11.0" "1.5.2")
+        (case (range "8.7" "8.11") (range "1.8" "1.10") "1.5.0")
+        (case (range "8.7" "8.10") (range "1.8" "1.10") "1.4")
+        (case "8.6" (range "1.6" "1.7") "1.1")
+      ]
+      null;
   release = {
     "2.4.0".sha256 = "sha256-7zfIddRH+Sl4nhEPtS/lMZwRUZI45AVFpcC/UC8Z0Yo=";
     "2.3.0".sha256 = "sha256-usIcxHOAuN+f/j3WjVbPrjz8Hl9ac8R6kYeAKi3CEts=";
diff --git a/pkgs/development/coq-modules/odd-order/default.nix b/pkgs/development/coq-modules/odd-order/default.nix
index 9c0b721141fc..81a59e31e291 100644
--- a/pkgs/development/coq-modules/odd-order/default.nix
+++ b/pkgs/development/coq-modules/odd-order/default.nix
@@ -18,16 +18,17 @@ mkCoqDerivation {
 
   inherit version;
   defaultVersion =
+    let
+      case = case: out: { inherit case out; };
+    in
     with lib.versions;
-    lib.switch mathcomp.character.version (lib.lists.sort (x: y: isLe x.out y.out) (
-      lib.mapAttrsToList (out: case: { inherit case out; }) {
-        "2.2.0" = (range "2.2.0" "2.4.0");
-        "2.1.0" = (range "2.1.0" "2.3.0");
-        "1.14.0" = (range "1.13.0" "1.15.0");
-        "1.13.0" = (range "1.12.0" "1.14.0");
-        "1.12.0" = (range "1.10.0" "1.12.0");
-      }
-    )) null;
+    lib.switch mathcomp.character.version [
+      (case ((range "2.2.0" "2.4.0")) "2.2.0")
+      (case ((range "2.1.0" "2.3.0")) "2.1.0")
+      (case ((range "1.13.0" "1.15.0")) "1.14.0")
+      (case ((range "1.12.0" "1.14.0")) "1.13.0")
+      (case ((range "1.10.0" "1.12.0")) "1.12.0")
+    ] null;
 
   propagatedBuildInputs = [
     mathcomp.character
diff --git a/pkgs/development/coq-modules/reglang/default.nix b/pkgs/development/coq-modules/reglang/default.nix
index d3d1bfc15ff9..819adb3fdd88 100644
--- a/pkgs/development/coq-modules/reglang/default.nix
+++ b/pkgs/development/coq-modules/reglang/default.nix
@@ -20,21 +20,25 @@ mkCoqDerivation {
 
   inherit version;
   defaultVersion =
-    with lib.versions;
     let
-      cmc = c: mc: [
-        c
-        mc
-      ];
+      case = coq: mc: out: {
+        case = [
+          coq
+          mc
+        ];
+        inherit out;
+      };
     in
-    lib.switch [ coq.coq-version mathcomp.version ] (lib.lists.sort (x: y: isLe x.out y.out) (
-      lib.mapAttrsToList (out: cases: { inherit cases out; }) {
-        "1.2.2" = cmc (range "8.16" "9.0") (range "2.0.0" "2.4.0");
-        "1.2.1" = cmc (range "8.16" "9.0") (range "2.0.0" "2.3.0");
-        "1.2.0" = cmc (range "8.16" "8.18") (range "2.0.0" "2.1.0");
-        "1.1.3" = cmc (range "8.10" "8.20") (isLt "2.0.0");
-      }
-    )) null;
+    with lib.versions;
+    lib.switch
+      [ coq.coq-version mathcomp.version ]
+      [
+        (case (range "8.16" "9.0") (range "2.0.0" "2.4.0") "1.2.2")
+        (case (range "8.16" "9.0") (range "2.0.0" "2.3.0") "1.2.1")
+        (case (range "8.16" "8.18") (range "2.0.0" "2.1.0") "1.2.0")
+        (case (range "8.10" "8.20") (isLt "2.0.0") "1.1.3")
+      ]
+      null;
 
   propagatedBuildInputs = [
     mathcomp.ssreflect
diff --git a/pkgs/development/coq-modules/relation-algebra/default.nix b/pkgs/development/coq-modules/relation-algebra/default.nix
index d512613fad9b..4f0302a72915 100644
--- a/pkgs/development/coq-modules/relation-algebra/default.nix
+++ b/pkgs/development/coq-modules/relation-algebra/default.nix
@@ -27,22 +27,23 @@ mkCoqDerivation {
 
   inherit version;
   defaultVersion =
+    let
+      case = case: out: { inherit case out; };
+    in
     with lib.versions;
-    lib.switch coq.coq-version (lib.lists.sort (x: y: isLe x.out y.out) (
-      lib.mapAttrsToList (out: case: { inherit case out; }) {
-        "1.7.11" = isEq "8.20";
-        "1.7.10" = range "8.18" "8.19";
-        "1.7.9" = isEq "8.17";
-        "1.7.8" = isEq "8.16";
-        "1.7.7" = isEq "8.15";
-        "1.7.6" = isEq "8.14";
-        "1.7.5" = isEq "8.13";
-        "1.7.4" = isEq "8.12";
-        "1.7.3" = isEq "8.11";
-        "1.7.2" = isEq "8.10";
-        "1.7.1" = isEq "8.9";
-      }
-    )) null;
+    lib.switch coq.coq-version [
+      (case (isEq "8.20") "1.7.11")
+      (case (range "8.18" "8.19") "1.7.10")
+      (case (isEq "8.17") "1.7.9")
+      (case (isEq "8.16") "1.7.8")
+      (case (isEq "8.15") "1.7.7")
+      (case (isEq "8.14") "1.7.6")
+      (case (isEq "8.13") "1.7.5")
+      (case (isEq "8.12") "1.7.4")
+      (case (isEq "8.11") "1.7.3")
+      (case (isEq "8.10") "1.7.2")
+      (case (isEq "8.9") "1.7.1")
+    ] null;
 
   mlPlugin = true;
 
diff --git a/pkgs/development/coq-modules/simple-io/default.nix b/pkgs/development/coq-modules/simple-io/default.nix
index d2a3ae0a26df..cc8c427619fb 100644
--- a/pkgs/development/coq-modules/simple-io/default.nix
+++ b/pkgs/development/coq-modules/simple-io/default.nix
@@ -13,14 +13,15 @@
   repo = "coq-simple-io";
   inherit version;
   defaultVersion =
+    let
+      case = case: out: { inherit case out; };
+    in
     with lib.versions;
-    lib.switch coq.coq-version (lib.lists.sort (x: y: isLe x.out y.out) (
-      lib.mapAttrsToList (out: case: { inherit case out; }) {
-        "1.10.0" = range "8.17" "9.0";
-        "1.8.0" = range "8.11" "8.19";
-        "1.3.0" = range "8.7" "8.13";
-      }
-    )) null;
+    lib.switch coq.coq-version [
+      (case (range "8.17" "9.0") "1.10.0")
+      (case (range "8.11" "8.19") "1.8.0")
+      (case (range "8.7" "8.13") "1.3.0")
+    ] null;
   release."1.10.0".sha256 = "sha256-67cBhLvRMWLWBL7NXK1zZTQC4PtSKu9qtesU4SqKkOw=";
   release."1.8.0".sha256 = "sha256-3ADNeXrBIpYRlfUW+LkLHUWV1w1HFrVc/TZISMuwvRY=";
   release."1.7.0".sha256 = "sha256:1a1q9x2abx71hqvjdai3n12jxzd49mhf3nqqh3ya2ssl2lj609ci";
diff --git a/pkgs/development/coq-modules/ssprove/default.nix b/pkgs/development/coq-modules/ssprove/default.nix
index b91ef56a36b7..2d11562ba084 100644
--- a/pkgs/development/coq-modules/ssprove/default.nix
+++ b/pkgs/development/coq-modules/ssprove/default.nix
@@ -18,28 +18,32 @@
 
   inherit version;
   defaultVersion =
-    with lib.versions;
     let
-      cmc = c: mc: [
-        c
-        mc
-      ];
+      case = coq: mc: out: {
+        case = [
+          coq
+          mc
+        ];
+        inherit out;
+      };
     in
-    lib.switch [ coq.coq-version mathcomp-boot.version ] (lib.lists.sort (x: y: isLe x.out y.out) (
-      lib.mapAttrsToList (out: cases: { inherit cases out; }) {
-        "0.2.4" = cmc (range "8.18" "9.0") (range "2.3.0" "2.4.0");
-        "0.2.3" = cmc (range "8.18" "8.20") (range "2.3.0" "2.3.0");
-        "0.2.2" = cmc (range "8.18" "8.20") (range "2.1.0" "2.2.0");
+    with lib.versions;
+    lib.switch
+      [ coq.coq-version mathcomp-boot.version ]
+      [
+        (case (range "8.18" "9.0") (range "2.3.0" "2.4.0") "0.2.4")
+        (case (range "8.18" "8.20") (range "2.3.0" "2.3.0") "0.2.3")
+        (case (range "8.18" "8.20") (range "2.1.0" "2.2.0") "0.2.2")
         # This is the original dependency:
-        # "0.1.0" = ["8.17" "1.18.0"];
+        # (case "8.17" "1.18.0" "0.1.0")
         # But it is not loadable. The math-comp nixpkgs configuration
         # will always only output version 1.18.0 for Coq 8.17.
         # Hence, the Coq 8.17 and math-comp 1.17.0 must be explicitly set
         # to load it.
         # (This version is not on the math-comp CI and hence not checked.)
-        "0.1.0" = cmc "8.17" "1.17.0";
-      }
-    )) null;
+        (case "8.17" "1.17.0" "0.1.0")
+      ]
+      null;
 
   releaseRev = v: "v${v}";
 
diff --git a/pkgs/development/coq-modules/stalmarck/default.nix b/pkgs/development/coq-modules/stalmarck/default.nix
index 2da766715881..e493321d8a0a 100644
--- a/pkgs/development/coq-modules/stalmarck/default.nix
+++ b/pkgs/development/coq-modules/stalmarck/default.nix
@@ -9,12 +9,13 @@
 let
   repo = "stalmarck";
   defaultVersion =
+    let
+      case = case: out: { inherit case out; };
+    in
     with lib.versions;
-    lib.switch coq.coq-version (lib.lists.sort (x: y: isLe x.out y.out) (
-      lib.mapAttrsToList (out: case: { inherit case out; }) {
-        "8.20.0" = isEq "8.20";
-      }
-    )) null;
+    lib.switch coq.coq-version [
+      (case (isEq "8.20") "8.20.0")
+    ] null;
   release = {
     "8.20.0".sha256 = "sha256-jITxQT1jLyZvWCGPnmK8i3IrwsZwMPOV0aBe9r22TIQ=";
   };
diff --git a/pkgs/development/coq-modules/stdlib/default.nix b/pkgs/development/coq-modules/stdlib/default.nix
index 90933aa24d75..474fd188afdf 100644
--- a/pkgs/development/coq-modules/stdlib/default.nix
+++ b/pkgs/development/coq-modules/stdlib/default.nix
@@ -14,13 +14,14 @@
 
   inherit version;
   defaultVersion =
+    let
+      case = case: out: { inherit case out; };
+    in
     with lib.versions;
-    lib.switch coq.coq-version (lib.lists.sort (x: y: isLe x.out y.out) (
-      lib.mapAttrsToList (out: case: { inherit case out; }) {
-        "9.0.0" = isLe "9.0";
-        # the < 9.0 above is artificial as stdlib was included in Coq before
-      }
-    )) null;
+    lib.switch coq.coq-version [
+      (case (isLe "9.0") "9.0.0")
+      # the < 9.0 above is artificial as stdlib was included in Coq before
+    ] null;
   releaseRev = v: "V${v}";
 
   release."9.0.0".sha256 = "sha256-2l7ak5Q/NbiNvUzIVXOniEneDXouBMNSSVFbD1Pf8cQ=";
diff --git a/pkgs/development/coq-modules/stdpp/default.nix b/pkgs/development/coq-modules/stdpp/default.nix
index 41eaacb7fde9..3f64dc57f47c 100644
--- a/pkgs/development/coq-modules/stdpp/default.nix
+++ b/pkgs/development/coq-modules/stdpp/default.nix
@@ -12,18 +12,19 @@ mkCoqDerivation {
   domain = "gitlab.mpi-sws.org";
   owner = "iris";
   defaultVersion =
+    let
+      case = case: out: { inherit case out; };
+    in
     with lib.versions;
-    lib.switch coq.coq-version (lib.lists.sort (x: y: isLe x.out y.out) (
-      lib.mapAttrsToList (out: case: { inherit case out; }) {
-        "1.11.0" = range "8.19" "9.0";
-        "1.10.0" = range "8.18" "8.19";
-        "1.9.0" = range "8.16" "8.18";
-        "1.8.0" = range "8.13" "8.17";
-        "1.6.0" = range "8.12" "8.14";
-        "1.5.0" = range "8.11" "8.13";
-        "1.4.0" = range "8.8" "8.10";
-      }
-    )) null;
+    lib.switch coq.coq-version [
+      (case (range "8.19" "9.0") "1.11.0")
+      (case (range "8.18" "8.19") "1.10.0")
+      (case (range "8.16" "8.18") "1.9.0")
+      (case (range "8.13" "8.17") "1.8.0")
+      (case (range "8.12" "8.14") "1.6.0")
+      (case (range "8.11" "8.13") "1.5.0")
+      (case (range "8.8" "8.10") "1.4.0")
+    ] null;
   release."1.11.0".sha256 = "sha256-yqnkaA5gUdZBJZ3JnvPYh11vKQRl0BAnior1yGowG7k=";
   release."1.10.0".sha256 = "sha256-bfynevIKxAltvt76lsqVxBmifFkzEhyX8lRgTKxr21I=";
   release."1.9.0".sha256 = "sha256-OXeB+XhdyzWMp5Karsz8obp0rTeMKrtG7fu/tmc9aeI=";
diff --git a/pkgs/development/rocq-modules/bignums/default.nix b/pkgs/development/rocq-modules/bignums/default.nix
index 3eced2572c69..238e16b3f9ce 100644
--- a/pkgs/development/rocq-modules/bignums/default.nix
+++ b/pkgs/development/rocq-modules/bignums/default.nix
@@ -11,12 +11,13 @@ mkRocqDerivation {
   owner = "coq";
   inherit version;
   defaultVersion =
+    let
+      case = case: out: { inherit case out; };
+    in
     with lib.versions;
-    lib.switch rocq-core.rocq-version (lib.lists.sort (x: y: isLe x.out y.out) (
-      lib.mapAttrsToList (out: case: { inherit case out; }) {
-        "9.0.0+rocq${rocq-core.rocq-version}" = range "9.0" "9.0";
-      }
-    )) null;
+    lib.switch rocq-core.rocq-version [
+      (case (range "9.0" "9.0") "9.0.0+rocq${rocq-core.rocq-version}")
+    ] null;
 
   release."9.0.0+rocq9.0".sha256 = "sha256-ctnwpyNVhryEUA5YEsAImrcJsNMhtBgDSOz+z5Z4R78=";
   releaseRev = v: "${if lib.versions.isGe "9.0" v then "v" else "V"}${v}";
diff --git a/pkgs/development/rocq-modules/hierarchy-builder/default.nix b/pkgs/development/rocq-modules/hierarchy-builder/default.nix
index 30be49a216e1..bb9efa9727cc 100644
--- a/pkgs/development/rocq-modules/hierarchy-builder/default.nix
+++ b/pkgs/development/rocq-modules/hierarchy-builder/default.nix
@@ -12,12 +12,13 @@ let
     owner = "math-comp";
     inherit version;
     defaultVersion =
+      let
+        case = case: out: { inherit case out; };
+      in
       with lib.versions;
-      lib.switch rocq-core.rocq-version (lib.lists.sort (x: y: isLe x.out y.out) (
-        lib.mapAttrsToList (out: case: { inherit case out; }) {
-          "1.9.1" = range "9.0" "9.0";
-        }
-      )) null;
+      lib.switch rocq-core.rocq-version [
+        (case (range "9.0" "9.0") "1.9.1")
+      ] null;
     release."1.9.1".sha256 = "sha256-AiS0ezMyfIYlXnuNsVLz1GlKQZzJX+ilkrKkbo0GrF0=";
     releaseRev = v: "v${v}";
 
diff --git a/pkgs/development/rocq-modules/rocq-elpi/default.nix b/pkgs/development/rocq-modules/rocq-elpi/default.nix
index 8d27cf2e0dfc..ea6ce3f6595e 100644
--- a/pkgs/development/rocq-modules/rocq-elpi/default.nix
+++ b/pkgs/development/rocq-modules/rocq-elpi/default.nix
@@ -12,11 +12,12 @@ let
     if elpi-version != null then
       elpi-version
     else
-      (lib.switch rocq-core.rocq-version (lib.lists.sort (x: y: lib.versions.isLe x.out y.out) (
-        lib.mapAttrsToList (out: case: { inherit case out; }) {
-          "2.0.7" = "9.0";
-        }
-      )) { });
+      let
+        case = case: out: { inherit case out; };
+      in
+      lib.switch rocq-core.rocq-version [
+        (case ("9.0") "2.0.7")
+      ] { };
   elpi = rocq-core.ocamlPackages.elpi.override { version = default-elpi-version; };
   propagatedBuildInputs_wo_elpi = [
     rocq-core.ocamlPackages.findlib
@@ -27,14 +28,13 @@ let
     repo = "coq-elpi";
     owner = "LPCIC";
     inherit version;
-    defaultVersion = lib.switch rocq-core.rocq-version (lib.lists.sort
-      (x: y: lib.versions.isLe x.out y.out)
-      (
-        lib.mapAttrsToList (out: case: { inherit case out; }) {
-          "2.5.2" = "9.0";
-        }
-      )
-    ) null;
+    defaultVersion =
+      let
+        case = case: out: { inherit case out; };
+      in
+      lib.switch rocq-core.rocq-version [
+        (case ("9.0") "2.5.2")
+      ] null;
     release."2.5.2".sha256 = "sha256-lLzjPrbVB3rrqox528YiheUb0u89R84Xmrgkn0oplOs=";
     releaseRev = v: "v${v}";
 
diff --git a/pkgs/development/rocq-modules/stdlib/default.nix b/pkgs/development/rocq-modules/stdlib/default.nix
index 17fe604d1df4..595080b1f92d 100644
--- a/pkgs/development/rocq-modules/stdlib/default.nix
+++ b/pkgs/development/rocq-modules/stdlib/default.nix
@@ -13,12 +13,13 @@ mkRocqDerivation {
 
   inherit version;
   defaultVersion =
+    let
+      case = case: out: { inherit case out; };
+    in
     with lib.versions;
-    lib.switch rocq-core.version (lib.lists.sort (x: y: isLe x.out y.out) (
-      lib.mapAttrsToList (out: case: { inherit case out; }) {
-        "9.0.0" = isEq "9.0";
-      }
-    )) null;
+    lib.switch rocq-core.version [
+      (case (isEq "9.0") "9.0.0")
+    ] null;
   releaseRev = v: "V${v}";
 
   release."9.0.0".sha256 = "sha256-2l7ak5Q/NbiNvUzIVXOniEneDXouBMNSSVFbD1Pf8cQ=";