diff --git a/pkgs/development/coq-modules/mtac2/default.nix b/pkgs/development/coq-modules/mtac2/default.nix
new file mode 100644
index 000000000000..8c2a96b4d781
--- /dev/null
+++ b/pkgs/development/coq-modules/mtac2/default.nix
@@ -0,0 +1,22 @@
+{ lib, mkCoqDerivation, coq, unicoq, version ? null }:
+
+mkCoqDerivation {
+  pname = "Mtac2";
+  owner = "Mtac2";
+  inherit version;
+  defaultVersion = with lib.versions; lib.switch coq.version [
+    { case = range "8.19" "8.19"; out = "1.4-coq${coq.coq-version}"; }
+  ] null;
+  release."1.4-coq8.19".sha256 = "sha256-G9eK0eLyECdT20/yf8yyz7M8Xq2WnHHaHpxVGP0yTtU=";
+  releaseRev = v: "v${v}";
+  mlPlugin = true;
+  propagatedBuildInputs = [ unicoq ];
+  meta = with lib; {
+    description = "Typed tactic language for Coq";
+    license = licenses.mit;
+  };
+  preBuild = ''
+    coq_makefile -f _CoqProject -o Makefile
+    patchShebangs tests/sf-5/configure.sh
+  '';
+}
diff --git a/pkgs/development/coq-modules/unicoq/default.nix b/pkgs/development/coq-modules/unicoq/default.nix
new file mode 100644
index 000000000000..c3167e4a9d7d
--- /dev/null
+++ b/pkgs/development/coq-modules/unicoq/default.nix
@@ -0,0 +1,20 @@
+{ lib, mkCoqDerivation, coq, version ? null }:
+
+mkCoqDerivation {
+  pname = "unicoq";
+  owner = "unicoq";
+  inherit version;
+  defaultVersion = with lib.versions; lib.switch coq.version [
+    { case = range "8.19" "8.19"; out = "1.6-${coq.coq-version}"; }
+  ] null;
+  release."1.6-8.19".sha256 = "sha256-fDk60B8AzJwiemxHGgWjNu6PTu6NcJoI9uK7Ww2AT14=";
+  releaseRev = v: "v${v}";
+  mlPlugin = true;
+  meta = with lib; {
+    description = "An enhanced unification algorithm for Coq";
+    license = licenses.mit;
+  };
+  preBuild = ''
+    coq_makefile -f _CoqProject -o Makefile
+  '';
+}
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index 8ab66479fd1f..8e78e3fe75e7 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -115,6 +115,7 @@ let
       metacoq-safechecker  = self.metacoq.safechecker;
       metacoq-erasure      = self.metacoq.erasure;
       metalib = callPackage ../development/coq-modules/metalib { };
+      mtac2 = callPackage ../development/coq-modules/mtac2 {};
       multinomials = callPackage ../development/coq-modules/multinomials {};
       odd-order = callPackage ../development/coq-modules/odd-order { };
       paco = callPackage ../development/coq-modules/paco {};
@@ -138,6 +139,7 @@ let
       tlc = callPackage ../development/coq-modules/tlc {};
       topology = callPackage ../development/coq-modules/topology {};
       trakt = callPackage ../development/coq-modules/trakt {};
+      unicoq = callPackage ../development/coq-modules/unicoq {};
       vcfloat = callPackage ../development/coq-modules/vcfloat (lib.optionalAttrs
         (lib.versions.range "8.16" "8.18" self.coq.version) {
           interval = self.interval.override { version = "4.9.0"; };