coqPackages.coq-tactical: init at unstable-2022-02-15 (#349179)

pkgs/development/coq-modules/coq-tactical/default.nix

@@ -0,0 +1,39 @@
+{
+  coq,
+  lib,
+  mkCoqDerivation,
+  version ? null,
+}:
+
+mkCoqDerivation {
+  pname = "coq-tactical";
+  owner = "tchajed";
+
+  inherit version;
+  displayVersion.coq-tactical = v: "unstable-${v}";
+  defaultVersion =
+    with lib.versions;
+    lib.switch coq.version [
+      {
+        case = range "8.11" "8.20";
+        out = "2022-02-15";
+      }
+    ] null;
+
+  release."2022-02-15" = {
+    rev = "7c26f9a017395c240845184dfed23489d29dbae5";
+    sha256 = "sha256-SNoQzGYw5tuabHUDwMAyUsAa/WNoYjmyR85b7a0hVl4=";
+  };
+
+  installPhase = ''
+    COQLIB=$out/lib/coq/${coq.coq-version}
+    mkdir -p $COQLIB/user-contrib/Tactical
+    cp -pR src/* $COQLIB/user-contrib/Tactical
+  '';
+
+  meta = {
+    description = "Library of Coq proof automation";
+    license = lib.licenses.mit;
+    maintainers = with lib.maintainers; [ stepbrobd ];
+  };
+}

pkgs/top-level/coq-packages.nix

@@ -47,6 +47,7 @@ let
       coq-haskell = callPackage ../development/coq-modules/coq-haskell { };
       coq-lsp = callPackage ../development/coq-modules/coq-lsp {};
       coq-record-update = callPackage ../development/coq-modules/coq-record-update { };
+      coq-tactical = callPackage ../development/coq-modules/coq-tactical {};
       coqeal = callPackage ../development/coq-modules/coqeal (
         (lib.optionalAttrs (lib.versions.range "8.13" "8.14" self.coq.coq-version) {
           bignums = self.bignums.override { version = "${self.coq.coq-version}.0"; };