Merge commit 'e19054ab3cd5b7cc9a01d0efc71c8fe310541065'

22 files changed, 58 insertions, 51 deletions

diff --git a/nixpkgs/pkgs/development/coq-modules/Cheerios/default.nix b/nixpkgs/pkgs/development/coq-modules/Cheerios/default.nix
index d58f65102190..4e75b9407dee 100644
--- a/nixpkgs/pkgs/development/coq-modules/Cheerios/default.nix
+++ b/nixpkgs/pkgs/development/coq-modules/Cheerios/default.nix
@@ -8,7 +8,7 @@ let param =
   };
 in
 
-stdenv.mkDerivation rec {
+stdenv.mkDerivation {
   name = "coq${coq.coq-version}-Cheerios-${param.version}";
 
   src = fetchFromGitHub {
diff --git a/nixpkgs/pkgs/development/coq-modules/InfSeqExt/default.nix b/nixpkgs/pkgs/development/coq-modules/InfSeqExt/default.nix
index 4fe86c3fae18..5df96519e7ff 100644
--- a/nixpkgs/pkgs/development/coq-modules/InfSeqExt/default.nix
+++ b/nixpkgs/pkgs/development/coq-modules/InfSeqExt/default.nix
@@ -8,7 +8,7 @@ let param =
   };
 in
 
-stdenv.mkDerivation rec {
+stdenv.mkDerivation {
   name = "coq${coq.coq-version}-InfSeqExt-${param.version}";
 
   src = fetchFromGitHub {
diff --git a/nixpkgs/pkgs/development/coq-modules/QuickChick/default.nix b/nixpkgs/pkgs/development/coq-modules/QuickChick/default.nix
index 874b99f2bebf..b99612894802 100644
--- a/nixpkgs/pkgs/development/coq-modules/QuickChick/default.nix
+++ b/nixpkgs/pkgs/development/coq-modules/QuickChick/default.nix
@@ -14,7 +14,7 @@ let params =
       sha256 = "0fri4nih40vfb0fbr82dsi631ydkw48xszinq43lyinpknf54y17";
     };
 
-    "8.8" = rec {
+    "8.8" = {
       version = "20190311";
       rev = "22af9e9a223d0038f05638654422e637e863b355";
       sha256 = "00rnr19lg6lg0haq1sy4ld38p7imzand6fc52fvfq27gblxkp2aq";
@@ -26,12 +26,12 @@ let params =
       sha256 = "1c34v1k37rk7v0xk2czv5n79mbjxjrm6nh3llg2mpfmdsqi68wf3";
     };
   };
-  param = params."${coq.coq-version}";
+  param = params.${coq.coq-version};
 in
 
 let recent = stdenv.lib.versionAtLeast coq.coq-version "8.8"; in
 
-stdenv.mkDerivation rec {
+stdenv.mkDerivation {
 
   name = "coq${coq.coq-version}-QuickChick-${param.version}";
 
diff --git a/nixpkgs/pkgs/development/coq-modules/StructTact/default.nix b/nixpkgs/pkgs/development/coq-modules/StructTact/default.nix
index e33b9427223e..2e4d12478b79 100644
--- a/nixpkgs/pkgs/development/coq-modules/StructTact/default.nix
+++ b/nixpkgs/pkgs/development/coq-modules/StructTact/default.nix
@@ -8,7 +8,7 @@ let param =
   };
 in
 
-stdenv.mkDerivation rec {
+stdenv.mkDerivation {
   name = "coq${coq.coq-version}-StructTact-${param.version}";
 
   src = fetchFromGitHub {
diff --git a/nixpkgs/pkgs/development/coq-modules/Velisarios/default.nix b/nixpkgs/pkgs/development/coq-modules/Velisarios/default.nix
index cd7ddfefb84a..92c9b2569ca4 100644
--- a/nixpkgs/pkgs/development/coq-modules/Velisarios/default.nix
+++ b/nixpkgs/pkgs/development/coq-modules/Velisarios/default.nix
@@ -20,10 +20,10 @@ let params =
       sha256 = "0l9885nxy0n955fj1gnijlxl55lyxiv9yjfmz8hmfrn9hl8vv1m2";
     };
   };
-  param = params."${coq.coq-version}";
+  param = params.${coq.coq-version};
 in
 
-stdenv.mkDerivation rec {
+stdenv.mkDerivation {
   name = "coq${coq.coq-version}-Velisarios-${param.version}";
 
   src = fetchFromGitHub {
diff --git a/nixpkgs/pkgs/development/coq-modules/Verdi/default.nix b/nixpkgs/pkgs/development/coq-modules/Verdi/default.nix
index 00d088a4a92c..d2e9660a630e 100644
--- a/nixpkgs/pkgs/development/coq-modules/Verdi/default.nix
+++ b/nixpkgs/pkgs/development/coq-modules/Verdi/default.nix
@@ -13,7 +13,7 @@ let param =
   };
 in
 
-stdenv.mkDerivation rec {
+stdenv.mkDerivation {
   name = "coq${coq.coq-version}-verdi-${param.version}";
 
   src = fetchFromGitHub {
diff --git a/nixpkgs/pkgs/development/coq-modules/bignums/default.nix b/nixpkgs/pkgs/development/coq-modules/bignums/default.nix
index a074b27ff658..fb45e591ec1a 100644
--- a/nixpkgs/pkgs/development/coq-modules/bignums/default.nix
+++ b/nixpkgs/pkgs/development/coq-modules/bignums/default.nix
@@ -22,10 +22,10 @@ let params = {
         sha256 = "1slw227idwjw9a21vj3s6kal22mrmvvlpg8r7xk590ml99bn6404";
       };
     };
-    param = params."${coq.coq-version}";
+    param = params.${coq.coq-version};
 in
 
-stdenv.mkDerivation rec {
+stdenv.mkDerivation {
 
   name = "coq${coq.coq-version}-bignums";
 
diff --git a/nixpkgs/pkgs/development/coq-modules/category-theory/default.nix b/nixpkgs/pkgs/development/coq-modules/category-theory/default.nix
index 3dfa95154d33..025a67a1e70b 100644
--- a/nixpkgs/pkgs/development/coq-modules/category-theory/default.nix
+++ b/nixpkgs/pkgs/development/coq-modules/category-theory/default.nix
@@ -19,10 +19,10 @@ let
     "8.8" = v20190414;
     "8.9" = v20190414;
   };
-  param = params."${coq.coq-version}";
+  param = params.${coq.coq-version};
 in
 
-stdenv.mkDerivation rec {
+stdenv.mkDerivation {
 
   name = "coq${coq.coq-version}-category-theory-${param.version}";
 
diff --git a/nixpkgs/pkgs/development/coq-modules/contribs/default.nix b/nixpkgs/pkgs/development/coq-modules/contribs/default.nix
index faf7db09ff9b..91fdb8651cc6 100644
--- a/nixpkgs/pkgs/development/coq-modules/contribs/default.nix
+++ b/nixpkgs/pkgs/development/coq-modules/contribs/default.nix
@@ -34,7 +34,7 @@ let mkContrib = repo: revs: param:
       rev = "86ac28259030649ef51460e4de2441c8a1017751";
       sha256 = "09bbk2a7pn0j76mmapl583f8a20zqd3a1m9lkml8rpwml692bzi9";
     };
-  }."${coq.coq-version}";
+  }.${coq.coq-version};
 
   abp = mkContrib "abp" [ "8.5" "8.6" "8.7" ] {
     version = "v8.6.0";
@@ -219,7 +219,7 @@ let mkContrib = repo: revs: param:
       rev = "aa33052c1edfc5a65885942a67c2773b5d96f8cc";
       sha256 = "0mjgfdr9bzsch0dlk4vq1frkaig14dqh46r54cv0l15flxapg0iw";
     };
-  }."${coq.coq-version}";
+  }.${coq.coq-version};
 
   continuations = mkContrib "continuations" [ ] {
     version = "v8.5.0-13-g6885310";
diff --git a/nixpkgs/pkgs/development/coq-modules/coq-elpi/default.nix b/nixpkgs/pkgs/development/coq-modules/coq-elpi/default.nix
index 04fc428b4092..c689cea1a827 100644
--- a/nixpkgs/pkgs/development/coq-modules/coq-elpi/default.nix
+++ b/nixpkgs/pkgs/development/coq-modules/coq-elpi/default.nix
@@ -7,7 +7,7 @@ let params = {
     sha256 = "188avk9irwjsbs5ya4ka01mpk3vw4397kv2rmsncqrrrsa1pdddk";
   };
 };
-  param = params."${coq.coq-version}";
+  param = params.${coq.coq-version};
 in
 
 stdenv.mkDerivation rec {
diff --git a/nixpkgs/pkgs/development/coq-modules/coq-ext-lib/default.nix b/nixpkgs/pkgs/development/coq-modules/coq-ext-lib/default.nix
index cade2bd352eb..898272d402b6 100644
--- a/nixpkgs/pkgs/development/coq-modules/coq-ext-lib/default.nix
+++ b/nixpkgs/pkgs/development/coq-modules/coq-ext-lib/default.nix
@@ -8,7 +8,7 @@ let params =
     "8.8" = { version = "0.9.8"; sha256 = "0z1ix855kdjl7zw5ca664h5njd1x8mmvf5wi37fck4dj9dgamwlz"; };
     "8.9" = { version = "0.10.1"; sha256 = "0r1vspad8fb8bry3zliiz4hfj4w1iib1l2gm115a94m6zbiksd95"; };
   };
-  param = params."${coq.coq-version}";
+  param = params.${coq.coq-version};
 in
 
 stdenv.mkDerivation rec {
diff --git a/nixpkgs/pkgs/development/coq-modules/coq-haskell/default.nix b/nixpkgs/pkgs/development/coq-modules/coq-haskell/default.nix
index 57f31e1847c1..e9263fb2be1e 100644
--- a/nixpkgs/pkgs/development/coq-modules/coq-haskell/default.nix
+++ b/nixpkgs/pkgs/development/coq-modules/coq-haskell/default.nix
@@ -26,10 +26,10 @@ let params =
       sha256 = "09dq1vvshhlhgjccrhqgbhnq2hrys15xryfszqq11rzpgvl2zgdv";
     };
   };
-  param = params."${coq.coq-version}";
+  param = params.${coq.coq-version};
 in
 
-stdenv.mkDerivation rec {
+stdenv.mkDerivation {
 
   name = "coq${coq.coq-version}-coq-haskell-${param.version}";
 
diff --git a/nixpkgs/pkgs/development/coq-modules/coqhammer/default.nix b/nixpkgs/pkgs/development/coq-modules/coqhammer/default.nix
index 28c651f9b16a..83a505017fbc 100644
--- a/nixpkgs/pkgs/development/coq-modules/coqhammer/default.nix
+++ b/nixpkgs/pkgs/development/coq-modules/coqhammer/default.nix
@@ -9,7 +9,7 @@ let
       sha256 = "0hmqwsry8ldg4g4hhwg4b84dgzibpdrg1wwsajhlyqfx3fb3n3b5";
     };
   };
-  param = params."${coq.coq-version}";
+  param = params.${coq.coq-version};
 in
 
 stdenv.mkDerivation rec {
diff --git a/nixpkgs/pkgs/development/coq-modules/coqprime/default.nix b/nixpkgs/pkgs/development/coq-modules/coqprime/default.nix
index c67342f1a2f7..6228bd4be9d0 100644
--- a/nixpkgs/pkgs/development/coq-modules/coqprime/default.nix
+++ b/nixpkgs/pkgs/development/coq-modules/coqprime/default.nix
@@ -15,7 +15,7 @@ let params =
     "8.9" = v_8_8;
     "8.10" = v_8_8;
     };
-  param = params."${coq.coq-version}"
+  param = params.${coq.coq-version}
 ; in
 
 stdenv.mkDerivation rec {
diff --git a/nixpkgs/pkgs/development/coq-modules/dpdgraph/default.nix b/nixpkgs/pkgs/development/coq-modules/dpdgraph/default.nix
index e403f7d4fb5c..401cb299497b 100644
--- a/nixpkgs/pkgs/development/coq-modules/dpdgraph/default.nix
+++ b/nixpkgs/pkgs/development/coq-modules/dpdgraph/default.nix
@@ -22,7 +22,7 @@ let params = {
     sha256 = "0qvar8gfbrcs9fmvkph5asqz4l5fi63caykx3bsn8zf0xllkwv0n";
   };
 };
-param = params."${coq.coq-version}";
+param = params.${coq.coq-version};
 in
 
 stdenv.mkDerivation {
diff --git a/nixpkgs/pkgs/development/coq-modules/equations/default.nix b/nixpkgs/pkgs/development/coq-modules/equations/default.nix
index 5446b540fac3..38444fe2b061 100644
--- a/nixpkgs/pkgs/development/coq-modules/equations/default.nix
+++ b/nixpkgs/pkgs/development/coq-modules/equations/default.nix
@@ -32,7 +32,7 @@ let
       sha256 = "1v5kx0xzxzsbs5r4w08rm1lrmjjggnd3ap0sd1my88ds17jzyasd";
     };
   };
-  param = params."${coq.coq-version}";
+  param = params.${coq.coq-version};
 in
 
 stdenv.mkDerivation rec {
diff --git a/nixpkgs/pkgs/development/coq-modules/iris/default.nix b/nixpkgs/pkgs/development/coq-modules/iris/default.nix
index ea26f3e1ca9d..0718e518b35c 100644
--- a/nixpkgs/pkgs/development/coq-modules/iris/default.nix
+++ b/nixpkgs/pkgs/development/coq-modules/iris/default.nix
@@ -1,15 +1,18 @@
-{ stdenv, fetchzip, coq, ssreflect, stdpp }:
+{ stdenv, fetchFromGitLab, coq, stdpp }:
 
 stdenv.mkDerivation rec {
-  version = "3.1.0";
+  version = "3.2.0";
   name = "coq${coq.coq-version}-iris-${version}";
-  src = fetchzip {
-    url = "https://gitlab.mpi-sws.org/FP/iris-coq/-/archive/iris-${version}/iris-coq-iris-${version}.tar.gz";
-    sha256 = "0ipdb061jj205avxifshxkpyxxqykigmlxk2n5nvxj62gs3rl5j1";
+  src = fetchFromGitLab {
+    domain = "gitlab.mpi-sws.org";
+    owner = "iris";
+    repo = "iris";
+    rev = "iris-${version}";
+    sha256 = "10dfi7qx6j5w6kbmbrf05xh18jwxr9iz5g7y0f6157msgvl081xs";
   };
 
   buildInputs = [ coq ];
-  propagatedBuildInputs = [ ssreflect stdpp ];
+  propagatedBuildInputs = [ stdpp ];
 
   enableParallelBuilding = true;
 
@@ -24,7 +27,7 @@ stdenv.mkDerivation rec {
   };
 
   passthru = {
-    compatibleCoqVersions = v: builtins.elem v [ "8.6" "8.7" "8.8" ];
+    compatibleCoqVersions = v: builtins.elem v [ "8.7" "8.8" "8.9" "8.10" ];
   };
 
 }
diff --git a/nixpkgs/pkgs/development/coq-modules/ltac2/default.nix b/nixpkgs/pkgs/development/coq-modules/ltac2/default.nix
index 30917fcb78f2..80b167aaa98a 100644
--- a/nixpkgs/pkgs/development/coq-modules/ltac2/default.nix
+++ b/nixpkgs/pkgs/development/coq-modules/ltac2/default.nix
@@ -17,7 +17,7 @@ let params = {
     sha256 = "0xby1kb26r9gcvk5511wqj05fqm9paynwfxlfqkmwkgnfmzk0x73";
   };
 };
-  param = params."${coq.coq-version}";
+  param = params.${coq.coq-version};
 in
 
 stdenv.mkDerivation rec {
diff --git a/nixpkgs/pkgs/development/coq-modules/mathcomp/default.nix b/nixpkgs/pkgs/development/coq-modules/mathcomp/default.nix
index d573eca809a2..6798236591c4 100644
--- a/nixpkgs/pkgs/development/coq-modules/mathcomp/default.nix
+++ b/nixpkgs/pkgs/development/coq-modules/mathcomp/default.nix
@@ -30,7 +30,7 @@ let
   # COMPUTED using the configuration above (edit with caution) #
   ##############################################################
   default-mathcomp-version = let v = head (
-    filter (mc: mathcomp-coq-versions."${mc}" coq.coq-version)
+    filter (mc: mathcomp-coq-versions.${mc} coq.coq-version)
             mathcomp-version-preference ++ ["0.0.0"]);
      in if v == "0.0.0" then max-mathcomp-version else v;
 
@@ -73,7 +73,7 @@ let
       custom-version = if is-released then mathcomp-version else "custom";
 
       # the base set of attributes for mathcomp
-      attrs = rec {
+      attrs = {
         name = "coq${coq.coq-version}-${pkgname}-${custom-version}";
 
         # used in ssreflect
@@ -126,9 +126,9 @@ let
         };
       };
     in
-    {"${mathcomp-pkg}" = stdenv.mkDerivation (attrs // overrides attrs);};
+    {${mathcomp-pkg} = stdenv.mkDerivation (attrs // overrides attrs);};
 
-getAttrOr = a: n: a."${n}" or (throw a.error);
+getAttrOr = a: n: a.${n} or (throw a.error);
 
 mathcompCorePkgs_1_7 = mathcompGen "1.7.0";
 mathcompCorePkgs_1_8 = mathcompGen "1.8.0";
@@ -136,7 +136,7 @@ mathcompCorePkgs_1_9 = mathcompGen "1.9.0";
 mathcompCorePkgs     = recurseIntoAttrs
   (mapDerivationAttrset dontDistribute (mathcompGen default-mathcomp-version));
 
-in rec {
+in {
 # mathcompGenSingle: given a version of mathcomp
 # generates an attribute set {single = <drv>;} with the single mathcomp derivation
 inherit mathcompGenSingle;
diff --git a/nixpkgs/pkgs/development/coq-modules/mathcomp/extra.nix b/nixpkgs/pkgs/development/coq-modules/mathcomp/extra.nix
index 0d9557623c36..c342c25a4118 100644
--- a/nixpkgs/pkgs/development/coq-modules/mathcomp/extra.nix
+++ b/nixpkgs/pkgs/development/coq-modules/mathcomp/extra.nix
@@ -139,7 +139,7 @@ packageGen = {
                                else compatibleCoqVersions;
     mc-core-deps = if builtins.isNull core-deps then [ssreflect] else core-deps;
   in
-  { "${package}" = let from = src; in
+  { ${package} = let from = src; in
 
   stdenv.mkDerivation rec {
     inherit version;
@@ -149,7 +149,7 @@ packageGen = {
       owner = owner;
       repo = package;
       rev = version;
-      sha256 = version-sha256."${version}";
+      sha256 = version-sha256.${version};
     } else from;
 
     propagatedBuildInputs = [ coq ] ++ mc-core-deps ++ extra-deps;
@@ -173,7 +173,7 @@ packageGen = {
   };
   };
 
-current-versions = versions."${current-ssreflect.version}" or {};
+current-versions = versions.${current-ssreflect.version} or {};
 
 select = x: mapAttrs (n: pkg: {package = n;} // pkg) (recursiveUpdate param x);
 
@@ -181,14 +181,14 @@ for-version = v: suffix: (mapAttrs' (n: pkg:
         {name = "mathcomp_${suffix}-${n}";
          value = (packageGen ({
              ssreflect = coqPackages."mathcomp-ssreflect_${suffix}";
-           } // pkg))."${n}";})
-        (select versions."${v}"));
+           } // pkg)).${n};})
+        (select versions.${v}));
 
 all = (for-version "1.7.0" "1_7") //
       (for-version "1.8.0" "1_8") //
       (for-version "1.9.0" "1_9") //
      (recurseIntoAttrs (mapDerivationAttrset dontDistribute (
-        mapAttrs' (n: pkg: {name = "mathcomp-${n}"; value = (packageGen pkg)."${n}";})
+        mapAttrs' (n: pkg: {name = "mathcomp-${n}"; value = (packageGen pkg).${n};})
               (select current-versions))));
 in
 {
diff --git a/nixpkgs/pkgs/development/coq-modules/paramcoq/default.nix b/nixpkgs/pkgs/development/coq-modules/paramcoq/default.nix
index 472d3aeb2d08..a8dd74dd5fb6 100644
--- a/nixpkgs/pkgs/development/coq-modules/paramcoq/default.nix
+++ b/nixpkgs/pkgs/development/coq-modules/paramcoq/default.nix
@@ -15,7 +15,7 @@ let params =
       sha256 = "002xabhjlph394vydw3dx8ipv5ry2nq3py4440bk9a18ljx0w6ll";
     };
   };
-  param = params."${coq.coq-version}";
+  param = params.${coq.coq-version};
 in
 
 stdenv.mkDerivation rec {
diff --git a/nixpkgs/pkgs/development/coq-modules/stdpp/default.nix b/nixpkgs/pkgs/development/coq-modules/stdpp/default.nix
index 883ed971b083..3ba99e87ffb6 100644
--- a/nixpkgs/pkgs/development/coq-modules/stdpp/default.nix
+++ b/nixpkgs/pkgs/development/coq-modules/stdpp/default.nix
@@ -1,10 +1,14 @@
-{ stdenv, fetchzip, coq }:
+{ stdenv, fetchFromGitLab, coq }:
 
-stdenv.mkDerivation {
-  name = "coq${coq.coq-version}-stdpp-1.1";
-  src = fetchzip {
-    url = "https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/-/archive/coq-stdpp-1.1.0/coq-stdpp-coq-stdpp-1.1.0.tar.gz";
-    sha256 = "0z8zl288x9w32w06sjax01jcpy12wd5i3ygps58dl2hfy7r3lwg0";
+stdenv.mkDerivation rec {
+  name = "coq${coq.coq-version}-stdpp-${version}";
+  version = "1.2.1";
+  src = fetchFromGitLab {
+    domain = "gitlab.mpi-sws.org";
+    owner = "iris";
+    repo = "stdpp";
+    rev = "coq-stdpp-${version}";
+    sha256 = "1lczybg1jq9drbi8nzrlb0k199x4n07aawjwfzrl3qqc0w8kmvdz";
   };
 
   buildInputs = [ coq ];
@@ -14,7 +18,7 @@ stdenv.mkDerivation {
   installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ];
 
   meta = {
-    homepage = "https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp";
+    inherit (src.meta) homepage;
     description = "An extended “Standard Library” for Coq";
     inherit (coq.meta) platforms;
     license = stdenv.lib.licenses.bsd3;
@@ -22,7 +26,7 @@ stdenv.mkDerivation {
   };
 
   passthru = {
-    compatibleCoqVersions = v: builtins.elem v [ "8.6" "8.7" "8.8" ];
+    compatibleCoqVersions = v: builtins.elem v [ "8.7" "8.8" "8.9" "8.10" ];
   };
 
 }