From 90e35645fc623215e9b5a0dca87a0e1aa8b5643f Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@gmail.com>
Date: Wed, 26 Jun 2024 06:32:52 +0200
Subject: [PATCH] coqPackages.coq-hammer: init at 1.3.2

---
 .../coq-modules/coq-hammer/default.nix        | 19 +++++++++++++++++++
 pkgs/top-level/coq-packages.nix               |  1 +
 2 files changed, 20 insertions(+)
 create mode 100644 pkgs/development/coq-modules/coq-hammer/default.nix

diff --git a/pkgs/development/coq-modules/coq-hammer/default.nix b/pkgs/development/coq-modules/coq-hammer/default.nix
new file mode 100644
index 000000000000..f332f0e3a82e
--- /dev/null
+++ b/pkgs/development/coq-modules/coq-hammer/default.nix
@@ -0,0 +1,19 @@
+{ lib, mkCoqDerivation, coq, coq-hammer-tactics, version ? null }:
+
+mkCoqDerivation {
+  inherit version;
+  pname = "coq-hammer";
+  inherit (coq-hammer-tactics) owner repo defaultVersion release releaseRev;
+
+  buildFlags = [ "plugin" ];
+  installTargets = [ "install-plugin" ];
+  extraInstallFlags = [ "BINDIR=$(out)/bin/" ];
+
+  mlPlugin = true;
+
+  propagatedBuildInputs = [ coq.ocamlPackages.findlib coq-hammer-tactics ];
+
+  meta = coq-hammer-tactics.meta // {
+    description = "General-purpose automated reasoning hammer tool for Coq";
+  };
+}
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index cc46214ce54c..bdbb53b1e0d1 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -38,6 +38,7 @@ let
       coq-bits = callPackage ../development/coq-modules/coq-bits {};
       coq-elpi = callPackage ../development/coq-modules/coq-elpi {};
       coq-ext-lib = callPackage ../development/coq-modules/coq-ext-lib {};
+      coq-hammer = callPackage ../development/coq-modules/coq-hammer { };
       coq-hammer-tactics = callPackage ../development/coq-modules/coq-hammer/tactics.nix { };
       coq-haskell = callPackage ../development/coq-modules/coq-haskell { };
       coq-lsp = callPackage ../development/coq-modules/coq-lsp {};