Commit 90e35645 authored by Vincent Laporte's avatar Vincent Laporte Committed by Vincent Laporte
Browse files

coqPackages.coq-hammer: init at 1.3.2

parent b8a048b9

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

0 → 100644
+19 −0
Original line number Diff line number Diff line 
{ 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";

  };

}

pkgs/top-level/coq-packages.nix

+1 −0
Original line number Diff line number Diff line
@@ -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 {};