1 files changed, 22 insertions, 0 deletions
diff --git a/nixpkgs/pkgs/development/coq-modules/mathcomp-tarjan/default.nix b/nixpkgs/pkgs/development/coq-modules/mathcomp-tarjan/default.nix
new file mode 100644
index 000000000000..6f82532ada30
--- /dev/null
+++ b/nixpkgs/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;
+  };
+}