diff options
| -rw-r--r-- | pkgs/development/coq-modules/mathcomp-algebra-tactics/default.nix | 23 | ||||
| -rw-r--r-- | pkgs/top-level/coq-packages.nix | 1 |
2 files changed, 24 insertions, 0 deletions
diff --git a/pkgs/development/coq-modules/mathcomp-algebra-tactics/default.nix b/pkgs/development/coq-modules/mathcomp-algebra-tactics/default.nix new file mode 100644 index 0000000000000..f4ae2afd38685 --- /dev/null +++ b/pkgs/development/coq-modules/mathcomp-algebra-tactics/default.nix @@ -0,0 +1,23 @@ +{ lib, mkCoqDerivation, coq, mathcomp-algebra, + coq-elpi, mathcomp-zify, version ? null }: + +with lib; mkCoqDerivation { + namePrefix = [ "coq" "mathcomp" ]; + pname = "algebra-tactics"; + owner = "math-comp"; + inherit version; + + defaultVersion = with versions; + switch [ coq.coq-version mathcomp-algebra.version ] [ + { cases = [ (range "8.13" "8.16") (isGe "1.12") ]; out = "1.0.0"; } + ] null; + + release."1.0.0".sha256 = "sha256-kszARPBizWbxSQ/Iqpf2vLbxYc6AjpUCLnSNlPcNfls="; + + propagatedBuildInputs = [ mathcomp-algebra coq-elpi mathcomp-zify ]; + + meta = { + description = "Ring and field tactics for Mathematical Components"; + maintainers = with maintainers; [ cohencyril ]; + }; +} diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix index 65de529685e3a..605988b588e85 100644 --- a/pkgs/top-level/coq-packages.nix +++ b/pkgs/top-level/coq-packages.nix @@ -82,6 +82,7 @@ let mathcomp-real-closed = callPackage ../development/coq-modules/mathcomp-real-closed {}; mathcomp-word = callPackage ../development/coq-modules/mathcomp-word {}; mathcomp-zify = callPackage ../development/coq-modules/mathcomp-zify {}; + mathcomp-algebra-tactics = callPackage ../development/coq-modules/mathcomp-algebra-tactics {}; mathcomp-tarjan = callPackage ../development/coq-modules/mathcomp-tarjan {}; metacoq = callPackage ../development/coq-modules/metacoq { }; metacoq-template-coq = self.metacoq.template-coq; |