diff --git a/pkgs/development/coq-modules/coqeal/default.nix b/pkgs/development/coq-modules/coqeal/default.nix
index ead8be66918d..c1810a3730c8 100644
--- a/pkgs/development/coq-modules/coqeal/default.nix
+++ b/pkgs/development/coq-modules/coqeal/default.nix
@@ -19,7 +19,7 @@ let
     defaultVersion =
       let
         case = coq: mc: out: {
-          case = [
+          cases = [
             coq
             mc
           ];
diff --git a/pkgs/development/coq-modules/deriving/default.nix b/pkgs/development/coq-modules/deriving/default.nix
index f2b61dccf5ba..bfa2e99a481e 100644
--- a/pkgs/development/coq-modules/deriving/default.nix
+++ b/pkgs/development/coq-modules/deriving/default.nix
@@ -15,7 +15,7 @@ mkCoqDerivation {
   defaultVersion =
     let
       case = coq: mc: out: {
-        case = [
+        cases = [
           coq
           mc
         ];
diff --git a/pkgs/development/coq-modules/extructures/default.nix b/pkgs/development/coq-modules/extructures/default.nix
index bab84dfc86b1..cfb2e819e22a 100644
--- a/pkgs/development/coq-modules/extructures/default.nix
+++ b/pkgs/development/coq-modules/extructures/default.nix
@@ -15,7 +15,7 @@
   defaultVersion =
     let
       case = coq: mc: out: {
-        case = [
+        cases = [
           coq
           mc
         ];
diff --git a/pkgs/development/coq-modules/fourcolor/default.nix b/pkgs/development/coq-modules/fourcolor/default.nix
index f55e55ffd5b3..7270ac6ffd14 100644
--- a/pkgs/development/coq-modules/fourcolor/default.nix
+++ b/pkgs/development/coq-modules/fourcolor/default.nix
@@ -24,7 +24,7 @@ mkCoqDerivation {
   defaultVersion =
     let
       case = coq: mc: out: {
-        case = [
+        cases = [
           coq
           mc
         ];
diff --git a/pkgs/development/coq-modules/gaia/default.nix b/pkgs/development/coq-modules/gaia/default.nix
index bc69b24b09cb..a716a1ad0363 100644
--- a/pkgs/development/coq-modules/gaia/default.nix
+++ b/pkgs/development/coq-modules/gaia/default.nix
@@ -24,7 +24,7 @@ mkCoqDerivation {
   defaultVersion =
     let
       case = coq: mc: out: {
-        case = [
+        cases = [
           coq
           mc
         ];
diff --git a/pkgs/development/coq-modules/graph-theory/default.nix b/pkgs/development/coq-modules/graph-theory/default.nix
index 57b89553b553..f600a46b4a93 100644
--- a/pkgs/development/coq-modules/graph-theory/default.nix
+++ b/pkgs/development/coq-modules/graph-theory/default.nix
@@ -26,7 +26,7 @@ mkCoqDerivation {
   defaultVersion =
     let
       case = coq: mc: out: {
-        case = [
+        cases = [
           coq
           mc
         ];
diff --git a/pkgs/development/coq-modules/jasmin/default.nix b/pkgs/development/coq-modules/jasmin/default.nix
index c58cba094a18..d7545d9bba62 100644
--- a/pkgs/development/coq-modules/jasmin/default.nix
+++ b/pkgs/development/coq-modules/jasmin/default.nix
@@ -16,7 +16,7 @@ mkCoqDerivation {
   defaultVersion =
     let
       case = coq: mc: out: {
-        case = [
+        cases = [
           coq
           mc
         ];
diff --git a/pkgs/development/coq-modules/mathcomp-abel/default.nix b/pkgs/development/coq-modules/mathcomp-abel/default.nix
index 9fb880f99c8f..833333392536 100644
--- a/pkgs/development/coq-modules/mathcomp-abel/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-abel/default.nix
@@ -20,7 +20,7 @@ mkCoqDerivation {
   defaultVersion =
     let
       case = coq: mc: out: {
-        case = [
+        cases = [
           coq
           mc
         ];
diff --git a/pkgs/development/coq-modules/mathcomp-algebra-tactics/default.nix b/pkgs/development/coq-modules/mathcomp-algebra-tactics/default.nix
index 8f1b2ab26d48..0bd7cd8a9fb9 100644
--- a/pkgs/development/coq-modules/mathcomp-algebra-tactics/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-algebra-tactics/default.nix
@@ -21,7 +21,7 @@ mkCoqDerivation {
   defaultVersion =
     let
       case = coq: mc: out: {
-        case = [
+        cases = [
           coq
           mc
         ];
diff --git a/pkgs/development/coq-modules/mathcomp-analysis/default.nix b/pkgs/development/coq-modules/mathcomp-analysis/default.nix
index f87d9ed34893..5a6ec833428f 100644
--- a/pkgs/development/coq-modules/mathcomp-analysis/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-analysis/default.nix
@@ -46,7 +46,7 @@ let
   defaultVersion =
     let
       case = coq: mc: out: {
-        case = [
+        cases = [
           coq
           mc
         ];
diff --git a/pkgs/development/coq-modules/mathcomp-apery/default.nix b/pkgs/development/coq-modules/mathcomp-apery/default.nix
index 45501f1969a0..3ae89da38c16 100644
--- a/pkgs/development/coq-modules/mathcomp-apery/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-apery/default.nix
@@ -19,7 +19,7 @@ mkCoqDerivation {
   defaultVersion =
     let
       case = coq: mc: out: {
-        case = [
+        cases = [
           coq
           mc
         ];
diff --git a/pkgs/development/coq-modules/mathcomp-finmap/default.nix b/pkgs/development/coq-modules/mathcomp-finmap/default.nix
index 82c1bf7ac48f..11b177e80910 100644
--- a/pkgs/development/coq-modules/mathcomp-finmap/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-finmap/default.nix
@@ -18,7 +18,7 @@ mkCoqDerivation {
   defaultVersion =
     let
       case = coq: mc: out: {
-        case = [
+        cases = [
           coq
           mc
         ];
diff --git a/pkgs/development/coq-modules/mathcomp-infotheo/default.nix b/pkgs/development/coq-modules/mathcomp-infotheo/default.nix
index 6a29a390174a..c3bb32a15cc5 100644
--- a/pkgs/development/coq-modules/mathcomp-infotheo/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-infotheo/default.nix
@@ -21,7 +21,7 @@
   defaultVersion =
     let
       case = coq: mc: out: {
-        case = [
+        cases = [
           coq
           mc
         ];
diff --git a/pkgs/development/coq-modules/mathcomp-tarjan/default.nix b/pkgs/development/coq-modules/mathcomp-tarjan/default.nix
index 383da1bd8231..e5f1b9ee1b9e 100644
--- a/pkgs/development/coq-modules/mathcomp-tarjan/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-tarjan/default.nix
@@ -20,7 +20,7 @@ mkCoqDerivation {
   defaultVersion =
     let
       case = coq: mc: out: {
-        case = [
+        cases = [
           coq
           mc
         ];
diff --git a/pkgs/development/coq-modules/mathcomp-word/default.nix b/pkgs/development/coq-modules/mathcomp-word/default.nix
index 555b572c467b..0041eca094ad 100644
--- a/pkgs/development/coq-modules/mathcomp-word/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-word/default.nix
@@ -58,7 +58,7 @@ mkCoqDerivation {
   defaultVersion =
     let
       case = coq: mc: out: {
-        case = [
+        cases = [
           coq
           mc
         ];
diff --git a/pkgs/development/coq-modules/mathcomp-zify/default.nix b/pkgs/development/coq-modules/mathcomp-zify/default.nix
index 8e4dd232dcff..e1d1a9fdec83 100644
--- a/pkgs/development/coq-modules/mathcomp-zify/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-zify/default.nix
@@ -22,7 +22,7 @@ mkCoqDerivation {
   defaultVersion =
     let
       case = coq: mc: out: {
-        case = [
+        cases = [
           coq
           mc
         ];
diff --git a/pkgs/development/coq-modules/multinomials/default.nix b/pkgs/development/coq-modules/multinomials/default.nix
index 8b2f7608afc8..bf6a7eaef0f3 100644
--- a/pkgs/development/coq-modules/multinomials/default.nix
+++ b/pkgs/development/coq-modules/multinomials/default.nix
@@ -22,7 +22,7 @@ mkCoqDerivation {
   defaultVersion =
     let
       case = coq: mc: out: {
-        case = [
+        cases = [
           coq
           mc
         ];
diff --git a/pkgs/development/coq-modules/odd-order/default.nix b/pkgs/development/coq-modules/odd-order/default.nix
index 81a59e31e291..82c0272c16f3 100644
--- a/pkgs/development/coq-modules/odd-order/default.nix
+++ b/pkgs/development/coq-modules/odd-order/default.nix
@@ -23,11 +23,11 @@ mkCoqDerivation {
     in
     with lib.versions;
     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")
+      (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 = [
diff --git a/pkgs/development/coq-modules/reglang/default.nix b/pkgs/development/coq-modules/reglang/default.nix
index 819adb3fdd88..adbb2bfbae98 100644
--- a/pkgs/development/coq-modules/reglang/default.nix
+++ b/pkgs/development/coq-modules/reglang/default.nix
@@ -22,7 +22,7 @@ mkCoqDerivation {
   defaultVersion =
     let
       case = coq: mc: out: {
-        case = [
+        cases = [
           coq
           mc
         ];
diff --git a/pkgs/development/coq-modules/ssprove/default.nix b/pkgs/development/coq-modules/ssprove/default.nix
index 2d11562ba084..1b8ad91a51b9 100644
--- a/pkgs/development/coq-modules/ssprove/default.nix
+++ b/pkgs/development/coq-modules/ssprove/default.nix
@@ -20,7 +20,7 @@
   defaultVersion =
     let
       case = coq: mc: out: {
-        case = [
+        cases = [
           coq
           mc
         ];