coqPackages.mathcomp-algebra-tactics: init at 1.0.0

{ 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 ];

  };

}

      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;