diff --git a/pkgs/development/coq-modules/coqeal/default.nix b/pkgs/development/coq-modules/coqeal/default.nix
index 7c3470fb4b72..3a1562b3386d 100644
--- a/pkgs/development/coq-modules/coqeal/default.nix
+++ b/pkgs/development/coq-modules/coqeal/default.nix
@@ -4,10 +4,10 @@
 with lib; mkCoqDerivation {
 
   pname = "CoqEAL";
-  owner = "CoqEAL";
+
   inherit version;
   defaultVersion = with versions; switch [ coq.version mathcomp.version ]  [
-      { cases = [ (isGe "8.10") "1.12.0" ]; out = "1.0.6"; }
+      { cases = [ (isGe "8.10") (isGe "1.12.0") ]; out = "1.0.6"; }
       { cases = [ (isGe "8.10") (range "1.11.0" "1.12.0") ]; out = "1.0.5"; }
       { cases = [ (isGe "8.7") "1.11.0" ]; out = "1.0.4"; }
       { cases = [ (isGe "8.7") "1.10.0" ]; out = "1.0.3"; }
diff --git a/pkgs/development/coq-modules/extructures/default.nix b/pkgs/development/coq-modules/extructures/default.nix
index c34fa76f6e05..c78c6ca03fc3 100644
--- a/pkgs/development/coq-modules/extructures/default.nix
+++ b/pkgs/development/coq-modules/extructures/default.nix
@@ -9,9 +9,9 @@ with lib;
   owner = "arthuraa";
 
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
-    { case = range "8.11" "8.14"; out = "0.3.0"; }
-    { case = range "8.10" "8.12"; out = "0.2.2"; }
+  defaultVersion = with versions; switch [coq.coq-version ssreflect.version] [
+    { cases = [(range "8.11" "8.14") (isLe "1.12.0") ]; out = "0.3.0"; }
+    { cases = [(range "8.10" "8.12") (isLe "1.12.0") ]; out = "0.2.2"; }
   ] null;
 
   releaseRev = v: "v${v}";
diff --git a/pkgs/development/coq-modules/gaia-hydras/default.nix b/pkgs/development/coq-modules/gaia-hydras/default.nix
index c20c503d73ba..5b76cb9148f0 100644
--- a/pkgs/development/coq-modules/gaia-hydras/default.nix
+++ b/pkgs/development/coq-modules/gaia-hydras/default.nix
@@ -1,4 +1,5 @@
-{ lib, mkCoqDerivation, coq, hydra-battles, gaia, mathcomp-zify, version ? null }:
+{ lib, mkCoqDerivation, coq, hydra-battles, gaia,
+  mathcomp-zify, mathcomp, version ? null }:
 
 with lib; mkCoqDerivation rec {
   pname = "gaia-hydras";
@@ -8,8 +9,8 @@ with lib; mkCoqDerivation rec {
   releaseRev = (v: "v${v}");
 
   inherit version;
-  defaultVersion = with versions; switch coq.coq-version [
-    { case = range "8.13" "8.14"; out = "0.5"; }
+  defaultVersion = with versions; switch [coq.coq-version mathcomp.version] [
+    { cases = [ (range "8.13" "8.14") (isGe "1.12.0") ]; out = "0.5"; }
   ] null;
 
   propagatedBuildInputs = [
diff --git a/pkgs/development/coq-modules/gaia/default.nix b/pkgs/development/coq-modules/gaia/default.nix
index 4c571f483e16..cf52916605e9 100644
--- a/pkgs/development/coq-modules/gaia/default.nix
+++ b/pkgs/development/coq-modules/gaia/default.nix
@@ -5,11 +5,12 @@ with lib; mkCoqDerivation {
 
   release."1.11".sha256 = "sha256:0gwb0blf37sv9gb0qpn34dab71zdcx7jsnqm3j9p58qw65cgsqn5";
   release."1.12".sha256 = "sha256:0c6cim4x6f9944g8v0cp0lxs244lrhb04ms4y2s6y1wh321zj5mi";
+  release."1.13".sha256 = "sha256:0i8ix2rbw10v34bi0yrx0z89ng96ydqbxm8rv2rnfgy4d1b27x6q";
   releaseRev = (v: "v${v}");
 
   inherit version;
   defaultVersion = with versions; switch [ coq.version mathcomp.version ] [
-    { cases = [ (range "8.10" "8.14") "1.12.0" ]; out = "1.12"; }
+    { cases = [ (range "8.10" "8.14") (isGe "1.12.0") ]; out = "1.13"; }
     { cases = [ (range "8.10" "8.12") "1.11.0" ]; out = "1.11"; }
   ] null;
 
diff --git a/pkgs/development/coq-modules/mathcomp-abel/default.nix b/pkgs/development/coq-modules/mathcomp-abel/default.nix
index 2a8c006b27cb..2ada5ee1c91c 100644
--- a/pkgs/development/coq-modules/mathcomp-abel/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-abel/default.nix
@@ -6,13 +6,17 @@ mkCoqDerivation {
   pname = "abel";
   owner = "math-comp";
 
-  release."1.0.0".sha256 = "190jd8hb8anqsvr9ysr514pm5sh8qhw4030ddykvwxx9d9q6rbp3";
-
   inherit version;
   defaultVersion = with lib; with versions; switch [ coq.version mathcomp.version ]  [
-      { cases = [ (range "8.10" "8.13") (range "1.11.0" "1.12.0") ]; out = "1.0.0"; }
+      { cases = [ (range "8.10" "8.14") (range "1.12.0" "1.13.0") ]; out = "1.2.0"; }
+      { cases = [ (range "8.10" "8.14") (range "1.11.0" "1.12.0") ]; out = "1.1.2"; }
     ] null;
 
+  release."1.2.0".sha256 = "1picd4m85ipj22j3b84cv8ab3330radzrhd6kp0gpxq14dhv02c2";
+  release."1.1.2".sha256 = "0565w713z1cwxvvdlqws2z5lgdys8lddf0vpwfdj7bpd7pq9hwxg";
+  release."1.0.0".sha256 = "190jd8hb8anqsvr9ysr514pm5sh8qhw4030ddykvwxx9d9q6rbp3";
+
+
   propagatedBuildInputs = [ mathcomp.field mathcomp-real-closed ];
 
   meta = with lib; {
diff --git a/pkgs/development/coq-modules/mathcomp-analysis/default.nix b/pkgs/development/coq-modules/mathcomp-analysis/default.nix
index 76a5a84cc233..5901fe2bb396 100644
--- a/pkgs/development/coq-modules/mathcomp-analysis/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-analysis/default.nix
@@ -18,7 +18,7 @@ let mca = mkCoqDerivation {
 
   inherit version;
   defaultVersion = with versions; switch [ coq.version mathcomp.version ]  [
-      { cases = [ (range "8.11" "8.13") "1.12.0" ];             out = "0.3.10"; }
+      { cases = [ (range "8.11" "8.14") (isGe "1.12.0") ];      out = "0.3.10"; }
       { cases = [ (range "8.11" "8.13") "1.11.0" ];             out = "0.3.4"; }
       { cases = [ (range "8.10" "8.12") "1.11.0" ];             out = "0.3.3"; }
       { cases = [ (range "8.10" "8.11") "1.11.0" ];             out = "0.3.1"; }
diff --git a/pkgs/development/coq-modules/mathcomp-finmap/default.nix b/pkgs/development/coq-modules/mathcomp-finmap/default.nix
index c506d07e4574..6a72f73a01b8 100644
--- a/pkgs/development/coq-modules/mathcomp-finmap/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-finmap/default.nix
@@ -7,7 +7,7 @@ with lib; mkCoqDerivation {
   owner = "math-comp";
   inherit version;
   defaultVersion = with versions; switch [ coq.version mathcomp.version ]  [
-      { cases = [ (isGe "8.10")          (range "1.11" "1.12") ]; out = "1.5.1"; }
+      { cases = [ (isGe "8.10")          (range "1.11" "1.13") ]; out = "1.5.1"; }
       { cases = [ (range "8.7" "8.11")   "1.11.0" ];              out = "1.5.0"; }
       { cases = [ (isEq "8.11")          (range "1.8" "1.10") ];  out = "1.4.0+coq-8.11"; }
       { cases = [ (range "8.7" "8.11.0") (range "1.8" "1.10") ];  out = "1.4.0"; }
diff --git a/pkgs/development/coq-modules/mathcomp-real-closed/default.nix b/pkgs/development/coq-modules/mathcomp-real-closed/default.nix
index dbd1550c6a7a..0f0937d1e458 100644
--- a/pkgs/development/coq-modules/mathcomp-real-closed/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-real-closed/default.nix
@@ -17,7 +17,7 @@ with lib; mkCoqDerivation {
   };
 
   defaultVersion = with versions; switch [ coq.version mathcomp.version ]  [
-      { cases = [ (isGe "8.10")  "1.12.0" ]; out = "1.1.2"; }
+      { cases = [ (isGe "8.10")  (isGe "1.12.0") ]; out = "1.1.2"; }
       { cases = [ (isGe "8.7")   "1.11.0" ]; out = "1.1.1"; }
       { cases = [ (isGe "8.7")   (range "1.9.0" "1.10.0") ]; out = "1.0.4"; }
       { cases = [ (isGe "8.7")   "1.8.0"  ]; out = "1.0.3"; }
diff --git a/pkgs/development/coq-modules/mathcomp-tarjan/default.nix b/pkgs/development/coq-modules/mathcomp-tarjan/default.nix
new file mode 100644
index 000000000000..6f82532ada30
--- /dev/null
+++ b/pkgs/development/coq-modules/mathcomp-tarjan/default.nix
@@ -0,0 +1,22 @@
+{ coq, mkCoqDerivation, mathcomp-ssreflect, mathcomp-fingroup,
+  lib, version ? null }@args:
+with lib; mkCoqDerivation {
+
+  namePrefix = [ "coq" "mathcomp" ];
+  pname = "tarjan";
+  owner = "math-comp";
+
+  inherit version;
+  defaultVersion = with versions;
+    switch [ coq.version mathcomp-ssreflect.version ] [{
+      cases = [ (range "8.10" "8.14") (isGe "1.12.0") ]; out = "1.0.0";
+  }] null;
+  release."1.0.0".sha256 = "sha256:0r459r0makshzwlygw6kd4lpvdjc43b3x5y9aa8x77f2z5gymjq1";
+
+  propagatedBuildInputs = [ mathcomp-ssreflect mathcomp-fingroup ];
+
+  meta = {
+    description = "Proofs of Tarjan and Kosaraju connected components algorithms";
+    license = licenses.cecill-b;
+  };
+}
diff --git a/pkgs/development/coq-modules/mathcomp-zify/default.nix b/pkgs/development/coq-modules/mathcomp-zify/default.nix
index 6ed8e114d803..fd3f31d3fe0d 100644
--- a/pkgs/development/coq-modules/mathcomp-zify/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-zify/default.nix
@@ -1,14 +1,15 @@
 { lib, mkCoqDerivation, coq, mathcomp-algebra, version ? null }:
 
 with lib; mkCoqDerivation rec {
-  pname = "mathcomp-zify";
+  namePrefix = [ "coq" "mathcomp" ];
+  pname = "zify";
   repo = "mczify";
   owner = "math-comp";
   inherit version;
 
   defaultVersion = with versions;
      switch [ coq.coq-version mathcomp-algebra.version ] [
-       { cases = [ (range "8.13" "8.14") (isEq "1.12") ]; out = "1.1.0+1.12+8.13"; }
+       { cases = [ (range "8.13" "8.14") (isGe "1.12") ]; out = "1.1.0+1.12+8.13"; }
      ] null;
 
   release."1.0.0+1.12+8.13".sha256 = "1j533vx6lacr89bj1bf15l1a0s7rvrx4l00wyjv99aczkfbz6h6k";
diff --git a/pkgs/development/coq-modules/mathcomp/default.nix b/pkgs/development/coq-modules/mathcomp/default.nix
index ddbad5eea874..562d1f949250 100644
--- a/pkgs/development/coq-modules/mathcomp/default.nix
+++ b/pkgs/development/coq-modules/mathcomp/default.nix
@@ -19,7 +19,8 @@ let
   owner = "math-comp";
   withDoc = single && (args.withDoc or false);
   defaultVersion = with versions; switch coq.coq-version [
-      { case = isGe  "8.10";        out = "1.12.0"; }
+      { case = isGe  "8.14";        out = "1.13.0"; }
+      { case = range "8.10" "8.13"; out = "1.12.0"; }
       { case = range "8.7"  "8.12"; out = "1.11.0"; }
       { case = range "8.7" "8.11";  out = "1.10.0"; }
       { case = range "8.7" "8.11";  out = "1.9.0";  }
@@ -28,6 +29,7 @@ let
       { case = range "8.5" "8.7";   out = "1.6.4";  }
     ] null;
   release = {
+    "1.13.0".sha256 = "0j4cz2y1r1aw79snkcf1pmicgzf8swbaf9ippz0vg99a572zqzri";
     "1.12.0".sha256 = "1ccfny1vwgmdl91kz5xlmhq4wz078xm4z5wpd0jy5rn890dx03wp";
     "1.11.0".sha256 = "06a71d196wd5k4wg7khwqb7j7ifr7garhwkd54s86i0j7d6nhl3c";
     "1.10.0".sha256 = "1b9m6pwxxyivw7rgx82gn5kmgv2mfv3h3y0mmjcjfypi8ydkrlbv";
diff --git a/pkgs/development/coq-modules/multinomials/default.nix b/pkgs/development/coq-modules/multinomials/default.nix
index 306e68ac0f05..c29669625a9d 100644
--- a/pkgs/development/coq-modules/multinomials/default.nix
+++ b/pkgs/development/coq-modules/multinomials/default.nix
@@ -9,7 +9,7 @@ with lib; mkCoqDerivation {
 
   inherit version;
   defaultVersion =  with versions; switch [ coq.version mathcomp.version ] [
-      { cases = [ (range "8.10" "8.14") "1.12.0" ];             out = "1.5.4"; }
+      { cases = [ (range "8.10" "8.14") (isGe "1.12.0") ];      out = "1.5.4"; }
       { cases = [ (range "8.10" "8.12") "1.12.0" ];             out = "1.5.3"; }
       { cases = [ (range "8.7" "8.12")  "1.11.0" ];             out = "1.5.2"; }
       { cases = [ (range "8.7" "8.11")  (range "1.8" "1.10") ]; out = "1.5.0"; }
diff --git a/pkgs/development/coq-modules/odd-order/default.nix b/pkgs/development/coq-modules/odd-order/default.nix
index adc4e3a59477..912d523d3bf7 100644
--- a/pkgs/development/coq-modules/odd-order/default.nix
+++ b/pkgs/development/coq-modules/odd-order/default.nix
@@ -10,7 +10,7 @@ mkCoqDerivation {
 
   inherit version;
   defaultVersion = with versions; switch mathcomp.character.version [
-    { case = pred.union (isGe "1.10.0") (isEq "dev"); out = "1.12.0"; }
+    { case = (range "1.10.0" "1.12.0"); out = "1.12.0"; }
   ] null;
 
   propagatedBuildInputs = [ mathcomp.character ];
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index 5feb98a17047..5e73426afbcb 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -74,6 +74,7 @@ let
       mathcomp-bigenough = callPackage ../development/coq-modules/mathcomp-bigenough {};
       mathcomp-real-closed = callPackage ../development/coq-modules/mathcomp-real-closed {};
       mathcomp-zify = callPackage ../development/coq-modules/mathcomp-zify {};
+      mathcomp-tarjan = callPackage ../development/coq-modules/mathcomp-tarjan {};
       metalib = callPackage ../development/coq-modules/metalib { };
       multinomials = callPackage ../development/coq-modules/multinomials {};
       odd-order = callPackage ../development/coq-modules/odd-order { };