Unverified Commit 8ff706ba authored by Weijia Wang's avatar Weijia Wang Committed by GitHub
Browse files

Merge pull request #212009 from Shawn8901/remove_with_lib_2 

treewide: remove global with lib; statements in pkgs/coq-modules
parents 1c399311 4dcb03a5

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

+2 −2
Original line number Diff line number Diff line 
{ lib, mkCoqDerivation, coq, StructTact, version ? null }:



with lib; mkCoqDerivation {

mkCoqDerivation {

  pname   = "cheerios";

  owner   = "uwplse";

  inherit version;

  defaultVersion = if versions.range "8.6" "8.16" coq.version then "20200201" else null;

  defaultVersion = if lib.versions.range "8.6" "8.16" coq.version then "20200201" else null;

  release."20200201".rev    = "9c7f66e57b91f706d70afa8ed99d64ed98ab367d";

  release."20200201".sha256 = "1h55s6lk47bk0lv5ralh81z55h799jbl9mhizmqwqzy57y8wqgs1";

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

+3 −3
Original line number Diff line number Diff line 
{ lib, mkCoqDerivation, coq, bignums, version ? null }:



with lib; mkCoqDerivation {

mkCoqDerivation {

  pname = "color";

  owner = "fblanqui";

  inherit version;

  defaultVersion = with versions; switch coq.version [

  defaultVersion = with lib.versions; lib.switch coq.version [

    {case = range "8.12" "8.16"; out = "1.8.2"; }

    {case = range "8.10" "8.11"; out = "1.7.0"; }

    {case = range "8.8"  "8.9";  out = "1.6.0"; }
@@ -26,6 +26,6 @@ with lib; mkCoqDerivation { 
  meta = {

    homepage = "https://github.com/fblanqui/color";

    description = "CoLoR is a library of formal mathematical definitions and proofs of theorems on rewriting theory and termination whose correctness has been mechanically checked by the Coq proof assistant.";

    maintainers = with maintainers; [ jpas jwiegley ];

    maintainers = with lib.maintainers; [ jpas jwiegley ];

  };

}

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

+3 −3
Original line number Diff line number Diff line 
{ lib, mkCoqDerivation, autoconf, automake, coq, version ? null }:



with lib; mkCoqDerivation {

mkCoqDerivation {

  pname = "HoTT";

  repo = "Coq-HoTT";

  owner = "HoTT";

  inherit version;

  defaultVersion = with versions; switch coq.coq-version [

  defaultVersion = with lib.versions; lib.switch coq.coq-version [

    { case = range "8.14" "8.16"; out = coq.coq-version; }

  ] null;

  releaseRev = v: "V${v}";
@@ -20,6 +20,6 @@ with lib; mkCoqDerivation { 
  meta = {

    homepage = "https://homotopytypetheory.org/";

    description = "Homotopy type theory";

    maintainers = with maintainers; [ siddharthist ];

    maintainers = with lib.maintainers; [ siddharthist ];

  };

}

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

+3 −3
Original line number Diff line number Diff line 
{ lib, mkCoqDerivation, coq, version ? null , paco, coq-ext-lib }:



with lib; mkCoqDerivation rec {

mkCoqDerivation rec {

  pname = "InteractionTrees";

  owner = "DeepSpec";

  inherit version;

  defaultVersion = with versions; switch coq.version [

  defaultVersion = with lib.versions; lib.switch coq.version [

    { case = range "8.10" "8.16";  out = "4.0.0"; }

  ] null;

  release."4.0.0".sha256 = "0h5rhndl8syc24hxq1gch86kj7mpmgr89bxp2hmf28fd7028ijsm";
@@ -12,6 +12,6 @@ with lib; mkCoqDerivation rec { 
  propagatedBuildInputs = [ coq-ext-lib paco ];

  meta = {

    description = "A Library for Representing Recursive and Impure Programs in Coq";

    maintainers = with maintainers; [ larsr ];

    maintainers = with lib.maintainers; [ larsr ];

  };

}

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

+2 −3
Original line number Diff line number Diff line 
{ lib, mkCoqDerivation, coq, version ? null }:



with lib;

mkCoqDerivation {

  pname = "LibHyps";

  owner = "Matafou";

  inherit version;

  defaultVersion = if (versions.range "8.11" "8.16") coq.version then "2.0.4.1" else null;

  defaultVersion = if (lib.versions.range "8.11" "8.16") coq.version then "2.0.4.1" else null;

  release = {

    "2.0.4.1".sha256 = "09p89701zhrfdmqlpxw3mziw8yylj1w1skb4b0xpbdwd1vsn4k3h";

  };
@@ -16,6 +15,6 @@ mkCoqDerivation { 


  meta = {

    description = "Hypotheses manipulation library";

    license = licenses.mit;

    license = lib.licenses.mit;

  };

}