diff --git a/pkgs/development/coq-modules/Cheerios/default.nix b/pkgs/development/coq-modules/Cheerios/default.nix
index 7506eb255d1a..60c2a7455303 100644
--- a/pkgs/development/coq-modules/Cheerios/default.nix
+++ b/pkgs/development/coq-modules/Cheerios/default.nix
@@ -16,7 +16,7 @@ mkCoqDerivation {
     in
     with lib.versions;
     lib.switch coq.version [
-      (case (range "8.14" "9.2") "20230107")
+      (case (range "8.14" "9.3") "20230107")
       (case (range "8.6" "8.16") "20200201")
     ] null;
   release."20230107".rev = "bad8ad2476e14df6b5a819b7aaddc27a7c53fb69";
diff --git a/pkgs/development/coq-modules/InfSeqExt/default.nix b/pkgs/development/coq-modules/InfSeqExt/default.nix
index 60949e27d6b7..3fcec1861e99 100644
--- a/pkgs/development/coq-modules/InfSeqExt/default.nix
+++ b/pkgs/development/coq-modules/InfSeqExt/default.nix
@@ -16,7 +16,7 @@ mkCoqDerivation {
     in
     with lib.versions;
     lib.switch coq.version [
-      (case (range "8.9" "9.2") "20230107")
+      (case (range "8.9" "9.3") "20230107")
       (case (range "8.5" "8.16") "20200131")
     ] null;
   release."20230107".rev = "601e89ec019501c48c27fcfc14b9a3c70456e408";
diff --git a/pkgs/development/coq-modules/Ordinal/default.nix b/pkgs/development/coq-modules/Ordinal/default.nix
index 84fc222204fa..9593afb9aa81 100644
--- a/pkgs/development/coq-modules/Ordinal/default.nix
+++ b/pkgs/development/coq-modules/Ordinal/default.nix
@@ -10,12 +10,12 @@ mkCoqDerivation {
   owner = "snu-sf";
   inherit version;
   defaultVersion =
+    let
+      case = case: out: { inherit case out; };
+    in
     with lib.versions;
-    lib.switch coq.version [
-      {
-        case = range "8.12" "9.2";
-        out = "0.5.6";
-      }
+    lib.switch coq.coq-version [
+      (case (range "8.12" "9.3") "0.5.6")
     ] null;
   release = {
     "0.5.6".hash = "sha256-ox9GaUsh/tWJGEPawPnNqXULI0kYglKmNmiTL8dF3uU=";
diff --git a/pkgs/development/coq-modules/StructTact/default.nix b/pkgs/development/coq-modules/StructTact/default.nix
index e5082fcd6593..25b09a3159b0 100644
--- a/pkgs/development/coq-modules/StructTact/default.nix
+++ b/pkgs/development/coq-modules/StructTact/default.nix
@@ -16,7 +16,7 @@ mkCoqDerivation {
     in
     with lib.versions;
     lib.switch coq.coq-version [
-      (case (range "8.9" "9.2") "20230107")
+      (case (range "8.9" "9.3") "20230107")
       (case (range "8.6" "8.16") "20210328")
       (case (range "8.5" "8.13") "20181102")
     ] null;
diff --git a/pkgs/development/coq-modules/ceres/default.nix b/pkgs/development/coq-modules/ceres/default.nix
index 9932f9559cff..abb0257bc023 100644
--- a/pkgs/development/coq-modules/ceres/default.nix
+++ b/pkgs/development/coq-modules/ceres/default.nix
@@ -19,7 +19,7 @@ mkCoqDerivation {
     in
     with lib.versions;
     lib.switch coq.version [
-      (case (range "8.14" "9.2") "0.4.1")
+      (case (range "8.14" "9.3") "0.4.1")
       (case (range "8.8" "8.16") "0.4.0")
     ] null;
   release."0.4.1".hash = "sha256-9vyk8/8IVsqNyhw3WPzl8w3L9Wu7gfaMVa3n2nWjFiA=";
diff --git a/pkgs/development/coq-modules/coq-record-update/default.nix b/pkgs/development/coq-modules/coq-record-update/default.nix
index 566d8dd4a368..51122574b96e 100644
--- a/pkgs/development/coq-modules/coq-record-update/default.nix
+++ b/pkgs/development/coq-modules/coq-record-update/default.nix
@@ -15,7 +15,7 @@ mkCoqDerivation {
     in
     with lib.versions;
     lib.switch coq.coq-version [
-      (case (range "8.14" "9.2") "0.3.6")
+      (case (range "8.14" "9.3") "0.3.6")
       (case (range "8.10" "9.1") "0.3.4")
     ] null;
   release."0.3.6".hash = "sha256-Sd9cmRPb/0MDlR9mzbFrrF9ifP/2vd0KG6u5fGOydds=";
diff --git a/pkgs/development/coq-modules/coqeal/default.nix b/pkgs/development/coq-modules/coqeal/default.nix
index 23f721b6bb00..20b8745cef9d 100644
--- a/pkgs/development/coq-modules/coqeal/default.nix
+++ b/pkgs/development/coq-modules/coqeal/default.nix
@@ -30,7 +30,7 @@ let
       lib.switch
         [ coq.coq-version mathcomp.version ]
         [
-          (case (range "9.0" "9.2") (isGe "2.5.0") "2.1.2")
+          (case (range "9.0" "9.3") (isGe "2.5.0") "2.1.2")
           (case (range "8.20" "9.1") (range "2.3.0" "2.5.0") "2.1.1")
           (case (range "8.20" "9.1") (range "2.3.0" "2.5.0") "2.1.0")
           (case (range "8.16" "8.20") (isGe "2.1.0") "2.0.3")
diff --git a/pkgs/development/coq-modules/coqutil/default.nix b/pkgs/development/coq-modules/coqutil/default.nix
index 0c7a1d393f2f..0c25603188db 100644
--- a/pkgs/development/coq-modules/coqutil/default.nix
+++ b/pkgs/development/coq-modules/coqutil/default.nix
@@ -18,7 +18,7 @@
       inherit (lib.versions) range;
     in
     lib.switch coq.version [
-      (case (range "9.0" "9.2") "0.0.7")
+      (case (range "9.0" "9.3") "0.0.7")
       (case (range "8.18" "8.20") "0.0.6")
       (case (range "8.17" "8.20") "0.0.5")
     ] null;
diff --git a/pkgs/development/coq-modules/flocq/default.nix b/pkgs/development/coq-modules/flocq/default.nix
index 8b88471229c0..601c8ae24898 100644
--- a/pkgs/development/coq-modules/flocq/default.nix
+++ b/pkgs/development/coq-modules/flocq/default.nix
@@ -20,7 +20,7 @@ let
       in
       with lib.versions;
       lib.switch coq.coq-version [
-        (case (range "8.15" "9.2") "4.2.2")
+        (case (range "8.15" "9.3") "4.2.2")
         (case (range "8.15" "9.1") "4.2.1")
         (case (range "8.14" "8.20") "4.2.0")
         (case (range "8.14" "8.18") "4.1.3")
diff --git a/pkgs/development/coq-modules/gaia/default.nix b/pkgs/development/coq-modules/gaia/default.nix
index abf16a0336f7..b048fe833367 100644
--- a/pkgs/development/coq-modules/gaia/default.nix
+++ b/pkgs/development/coq-modules/gaia/default.nix
@@ -36,7 +36,7 @@ mkCoqDerivation {
     lib.switch
       [ coq.coq-version mathcomp.version ]
       [
-        (case (range "8.16" "9.2") (range "2.0" "2.6") "2.4")
+        (case (range "8.16" "9.3") (range "2.0" "2.6") "2.4")
         (case (range "8.16" "9.1") (range "2.0" "2.5") "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")
diff --git a/pkgs/development/coq-modules/mathcomp-tarjan/default.nix b/pkgs/development/coq-modules/mathcomp-tarjan/default.nix
index d86510376a25..14db71813a3f 100644
--- a/pkgs/development/coq-modules/mathcomp-tarjan/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-tarjan/default.nix
@@ -31,7 +31,7 @@ mkCoqDerivation {
     lib.switch
       [ coq.coq-version mathcomp-ssreflect.version ]
       [
-        (case (range "8.16" "9.2") (range "2.0.0" "2.6.0") "1.0.5")
+        (case (range "8.16" "9.3") (range "2.0.0" "2.6.0") "1.0.5")
         (case (range "8.16" "9.1") (range "2.0.0" "2.5.0") "1.0.4")
         (case (range "8.16" "9.1") (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")
diff --git a/pkgs/development/coq-modules/paco/default.nix b/pkgs/development/coq-modules/paco/default.nix
index b6c648b26eaf..6f9103d2a597 100644
--- a/pkgs/development/coq-modules/paco/default.nix
+++ b/pkgs/development/coq-modules/paco/default.nix
@@ -16,7 +16,7 @@ mkCoqDerivation {
     in
     with lib.versions;
     lib.switch coq.coq-version [
-      (case (range "8.14" "9.2") "4.2.3")
+      (case (range "8.14" "9.3") "4.2.3")
       (case (isEq "8.13") "4.2.2")
       (case (range "8.12" "8.17") "4.1.2")
       (case (range "8.9" "8.13") "4.1.1")
diff --git a/pkgs/development/coq-modules/rewriter/default.nix b/pkgs/development/coq-modules/rewriter/default.nix
index d1822e1cd4bf..a5560bfde2d4 100644
--- a/pkgs/development/coq-modules/rewriter/default.nix
+++ b/pkgs/development/coq-modules/rewriter/default.nix
@@ -12,13 +12,11 @@ mkCoqDerivation {
   inherit version;
   defaultVersion =
     let
-      inherit (lib.versions) range;
+      case = case: out: { inherit case out; };
     in
+    with lib.versions;
     lib.switch coq.coq-version [
-      {
-        case = range "8.17" "9.2";
-        out = "0.0.15";
-      }
+      (case (range "8.17" "9.2") "0.0.15")
     ] null;
   release = {
     "0.0.15".hash = "sha256-zxNIMppFXUKShOXLbdZphy0Je5ii6cjcWUUcQMTcaHk=";
diff --git a/pkgs/development/rocq-modules/bignums/default.nix b/pkgs/development/rocq-modules/bignums/default.nix
index a3d6f931d6e0..f28cc74a3a55 100644
--- a/pkgs/development/rocq-modules/bignums/default.nix
+++ b/pkgs/development/rocq-modules/bignums/default.nix
@@ -16,7 +16,8 @@ mkRocqDerivation {
     in
     with lib.versions;
     lib.switch rocq-core.rocq-version [
-      (case (range "9.0" "9.2") "9.0.0+rocq${rocq-core.rocq-version}")
+      (case (range "9.2" "9.3") "9.0.0+rocq9.2")
+      (case (range "9.0" "9.1") "9.0.0+rocq${rocq-core.rocq-version}")
     ] null;
 
   release."9.0.0+rocq9.0".sha256 = "sha256-ctnwpyNVhryEUA5YEsAImrcJsNMhtBgDSOz+z5Z4R78=";
diff --git a/pkgs/development/rocq-modules/iris/default.nix b/pkgs/development/rocq-modules/iris/default.nix
index a3a2ebde58d0..b81ab29fa8bc 100644
--- a/pkgs/development/rocq-modules/iris/default.nix
+++ b/pkgs/development/rocq-modules/iris/default.nix
@@ -18,7 +18,7 @@ mkRocqDerivation {
     in
     with lib.versions;
     lib.switch rocq-core.rocq-version [
-      (case (range "9.0" "9.2") "4.5.0")
+      (case (range "9.0" "9.3") "4.5.0")
     ] null;
   release."4.5.0".sha256 = "sha256-oGqo+W1prLtAwRwo2U15VGhmrkDIPPE6uMbNrTa8iAQ=";
   releaseRev = v: "iris-${v}";
diff --git a/pkgs/development/rocq-modules/mathcomp-analysis/default.nix b/pkgs/development/rocq-modules/mathcomp-analysis/default.nix
index 96f83c3bb377..a1da2f0868b4 100644
--- a/pkgs/development/rocq-modules/mathcomp-analysis/default.nix
+++ b/pkgs/development/rocq-modules/mathcomp-analysis/default.nix
@@ -31,7 +31,7 @@ let
     lib.switch
       [ rocq-core.rocq-version mathcomp.version ]
       [
-        (case (range "9.0" "9.2") (range "2.4.0" "2.6.0") "1.16.0")
+        (case (range "9.0" "9.3") (range "2.4.0" "2.6.0") "1.16.0")
       ]
       null;
 
diff --git a/pkgs/development/rocq-modules/parseque/default.nix b/pkgs/development/rocq-modules/parseque/default.nix
index 12bf940b16a2..874fc0cbe496 100644
--- a/pkgs/development/rocq-modules/parseque/default.nix
+++ b/pkgs/development/rocq-modules/parseque/default.nix
@@ -13,15 +13,13 @@ mkRocqDerivation {
 
   inherit version;
   defaultVersion =
-    lib.switch
-      [ rocq-core.rocq-version ]
-      [
-        {
-          cases = [ (lib.versions.range "9.0" "9.2") ];
-          out = "0.3.1";
-        }
-      ]
-      null;
+    let
+      case = case: out: { inherit case out; };
+    in
+    with lib.versions;
+    lib.switch rocq-core.rocq-version [
+      (case (range "9.0" "9.3") "0.3.1")
+    ] null;
 
   release."0.3.0".sha256 = "sha256-W2eenv5Q421eVn2ubbninFmmdT875f3w/Zs7yGHUKP4=";
   release."0.3.1".sha256 = "sha256-t7nHpHl6E3iXkhMO0A53URmKVpWENjf/VODVXjD9Y1A=";
diff --git a/pkgs/development/rocq-modules/stdlib/default.nix b/pkgs/development/rocq-modules/stdlib/default.nix
index c7cbff5a5ce1..b16f2903937f 100644
--- a/pkgs/development/rocq-modules/stdlib/default.nix
+++ b/pkgs/development/rocq-modules/stdlib/default.nix
@@ -18,6 +18,7 @@ mkRocqDerivation {
     in
     with lib.versions;
     lib.switch rocq-core.version [
+      (case (range "9.3" "9.3") "9.2.0")
       (case (range "9.2" "9.2") "9.1.0")
       (case (range "9.0" "9.1") "9.0.0")
     ] null;
@@ -25,6 +26,7 @@ mkRocqDerivation {
 
   release."9.0.0".sha256 = "sha256-2l7ak5Q/NbiNvUzIVXOniEneDXouBMNSSVFbD1Pf8cQ=";
   release."9.1.0".sha256 = "sha256-D/kCMsJDg5OnP37GhvXIr2Fi/xCbgCCzoikKx5rL6p4=";
+  release."9.2.0".sha256 = "sha256-ySNY8XUQOH6B1B2p+39jdJ7UjIMrRDl499JJwpLEHuM=";
 
   mlPlugin = true;
 
diff --git a/pkgs/development/rocq-modules/stdpp/default.nix b/pkgs/development/rocq-modules/stdpp/default.nix
index 927fed975840..89c1b1eae2c9 100644
--- a/pkgs/development/rocq-modules/stdpp/default.nix
+++ b/pkgs/development/rocq-modules/stdpp/default.nix
@@ -17,7 +17,7 @@ mkRocqDerivation {
     in
     with lib.versions;
     lib.switch rocq-core.rocq-version [
-      (case (range "9.0" "9.2") "1.13.0")
+      (case (range "9.0" "9.3") "1.13.0")
     ] null;
   release."1.13.0".sha256 = "sha256-kj8oBzarsLB4DDQ43yz4ViQbyzuISqext28wC2Fh3Sw=";
   releaseRev = v: "stdpp-${v}";