diff --git a/pkgs/development/coq-modules/mathcomp-zify/default.nix b/pkgs/development/coq-modules/mathcomp-zify/default.nix new file mode 100644 index 00000000000..65af999d08f --- /dev/null +++ b/pkgs/development/coq-modules/mathcomp-zify/default.nix @@ -0,0 +1,22 @@ +{ lib, mkCoqDerivation, coq, mathcomp-algebra, version ? null }: + +with lib; mkCoqDerivation rec { + pname = "mathcomp-zify"; + repo = "mczify"; + owner = "math-comp"; + inherit version; + + defaultVersion = with versions; + switch [ coq.coq-version mathcomp-algebra.version ] [ + { cases = [ (isEq "8.13") (isEq "1.12") ]; out = "1.0.0+1.12+8.13"; } + ] null; + + release."1.0.0+1.12+8.13".sha256 = "1j533vx6lacr89bj1bf15l1a0s7rvrx4l00wyjv99aczkfbz6h6k"; + + propagatedBuildInputs = [ mathcomp-algebra ]; + + meta = { + description = "Micromega 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 9884553c9e0..2efd2c1849b 100644 --- a/pkgs/top-level/coq-packages.nix +++ b/pkgs/top-level/coq-packages.nix @@ -60,6 +60,7 @@ let mathcomp-finmap = callPackage ../development/coq-modules/mathcomp-finmap {}; mathcomp-bigenough = callPackage ../development/coq-modules/mathcomp-bigenough {}; mathcomp-real-closed = callPackage ../development/coq-modules/mathcomp-real-closed {}; + mathcomp-zify = callPackage ../development/coq-modules/mathcomp-zify {}; metalib = callPackage ../development/coq-modules/metalib { }; multinomials = callPackage ../development/coq-modules/multinomials {}; odd-order = callPackage ../development/coq-modules/odd-order { };