diff --git a/doc/languages-frameworks/coq.section.md b/doc/languages-frameworks/coq.section.md
index 9a692104a041..11777b5eef42 100644
--- a/doc/languages-frameworks/coq.section.md
+++ b/doc/languages-frameworks/coq.section.md
@@ -29,14 +29,19 @@ The recommended way of defining a derivation for a Coq library, is to use the `c
 * `releaseRev` (optional, defaults to `(v: v)`), provides a default mapping from release names to revision hashes/branch names/tags,
 * `displayVersion` (optional), provides a way to alter the computation of `name` from `pname`, by explaining how to display version numbers,
 * `namePrefix` (optional, defaults to `[ "coq" ]`), provides a way to alter the computation of `name` from `pname`, by explaining which dependencies must occur in `name`,
-* `extraNativeBuildInputs` (optional), by default `nativeBuildInputs` just contains `coq`, this allows to add more native build inputs, `nativeBuildInputs` are executables and `buildInputs` are libraries and dependencies,
-* `extraBuildInputs` (optional), this allows to add more build inputs,
-* `mlPlugin` (optional, defaults to `false`). Some extensions (plugins) might require OCaml and sometimes other OCaml packages. Standard dependencies can be added by setting the current option to `true`. For a finer grain control, the `coq.ocamlPackages` attribute can be used in `extraBuildInputs` to depend on the same package set Coq was built against.
-* `useDune2ifVersion` (optional, default to `(x: false)` uses Dune2 to build the package if the provided predicate evaluates to true on the version, e.g. `useDune2if = versions.isGe "1.1"`  will use dune if the version of the package is greater or equal to `"1.1"`,
+* `nativeBuildInputs` (optional), is a list of executables that are required to build the current derivation, in addition to the default ones (namely `which`, `dune` and `ocaml` depending on whether `useDune2`, `useDune2ifVersion` and `mlPlugin` are set).
+* `extraNativeBuildInputs` (optional, deprecated), an additional list of derivation to add to `nativeBuildInputs`,
+* `overrideNativeBuildInputs` (optional) replaces the default list of derivation to which `nativeBuildInputs` and `extraNativeBuildInputs` adds extra elements,
+* `buildInputs` (optional), is a list of libraries and dependencies that are required to build and run the current derivation, in addition to the default one `[ coq ]`,
+* `extraBuildInputs` (optional, deprecated), an additional list of derivation to add to `buildInputs`,
+* `overrideBuildInputs` (optional) replaces the default list of derivation to which `buildInputs` and `extraBuildInputs` adds extras elements,
+* `propagatedBuildInputs` (optional) is passed as is to `mkDerivation`, we recommend to use this for Coq libraries and Coq plugin dependencies, as this makes sure the paths of the compiled libraries and plugins will always be added to the build environements of subsequent derivation, which is necessary for Coq packages to work correctly,
+* `mlPlugin` (optional, defaults to `false`). Some extensions (plugins) might require OCaml and sometimes other OCaml packages. Standard dependencies can be added by setting the current option to `true`. For a finer grain control, the `coq.ocamlPackages` attribute can be used in `nativeBuildInputs`, `buildInputs`, and `propagatedBuildInputs` to depend on the same package set Coq was built against.
+* `useDune2ifVersion` (optional, default to `(x: false)` uses Dune2 to build the package if the provided predicate evaluates to true on the version, e.g. `useDune2ifVersion = versions.isGe "1.1"`  will use dune if the version of the package is greater or equal to `"1.1"`,
 * `useDune2` (optional, defaults to `false`) uses Dune2 to build the package if set to true, the presence of this attribute overrides the behavior of the previous one.
 * `opam-name` (optional, defaults to concatenating with a dash separator the components of `namePrefix` and `pname`), name of the Dune package to build.
 * `enableParallelBuilding` (optional, defaults to `true`), since it is activated by default, we provide a way to disable it.
-* `extraInstallFlags` (optional), allows to extend `installFlags` which initializes the variable `COQMF_COQLIB` so as to install in the proper subdirectory. Indeed Coq libraries should be installed in `$(out)/lib/coq/${coq.coq-version}/user-contrib/`. Such directories are automatically added to the `$COQPATH` environment variable by the hook defined in the Coq derivation.
+* `extraInstallFlags` (optional), allows to extend `installFlags` which initializes the variables `DESTDIR` and `COQMF_COQLIB` so as to install in the proper subdirectory. Indeed Coq libraries should be installed in `$(out)/lib/coq/${coq.coq-version}/user-contrib/`. Such directories are automatically added to the `$COQPATH` environment variable by the hook defined in the Coq derivation.
 * `setCOQBIN` (optional, defaults to `true`), by default, the environment variable `$COQBIN` is set to the current Coq's binary, but one can disable this behavior by setting it to `false`,
 * `useMelquiondRemake` (optional, default to `null`) is an attribute set, which, if given, overloads the `preConfigurePhases`, `configureFlags`, `buildPhase`, and `installPhase` attributes of the derivation for a specific use in libraries using `remake` as set up by Guillaume Melquiond for `flocq`, `gappalib`, `interval`, and `coquelicot` (see the corresponding derivation for concrete examples of use of this option). For backward compatibility, the attribute `useMelquiondRemake.logpath` must be set to the logical root of the library (otherwise, one can pass `useMelquiondRemake = {}` to activate this without backward compatibility).
 * `dropAttrs`, `keepAttrs`, `dropDerivationAttrs` are all optional and allow to tune which attribute is added or removed from the final call to `mkDerivation`.
diff --git a/maintainers/maintainer-list.nix b/maintainers/maintainer-list.nix
index 7b01e10bf9af..4f7e4f73c431 100644
--- a/maintainers/maintainer-list.nix
+++ b/maintainers/maintainer-list.nix
@@ -9572,8 +9572,8 @@
     githubId = 14816024;
     name = "oxalica";
     keys = [{
-      longkeyid = "rsa4096/0xCED392DE0C483D00";
-      fingerprint = "5CB0 E9E5 D5D5 71F5 7F54  0FEA CED3 92DE 0C48 3D00";
+      longkeyid = "ed25519/0x7571654CF88E31C2";
+      fingerprint = "F90F FD6D 585C 2BA1 F13D  E8A9 7571 654C F88E 31C2";
     }];
   };
   oxij = {
diff --git a/pkgs/applications/misc/1password/default.nix b/pkgs/applications/misc/1password/default.nix
index ffd4103e214e..080d7b0c9fb0 100644
--- a/pkgs/applications/misc/1password/default.nix
+++ b/pkgs/applications/misc/1password/default.nix
@@ -12,12 +12,12 @@ let
     if extension == "zip" then fetchzip args else fetchurl args;
 
   pname = "1password-cli";
-  version = "2.1.0";
+  version = "2.2.0";
   sources = rec {
-    aarch64-linux = fetch "linux_arm64" "sha256-DTYWqhawyAQBIxMUksZheyN8WSVPyhCghZC8orxKsBk=" "zip";
-    i686-linux = fetch "linux_386" "sha256-JBjiKxbJnFILSOVnOUIcY3GpbOT2UOJlasTSPRyYz4I=" "zip";
-    x86_64-linux = fetch "linux_amd64" "sha256-PfVOvUF8Rls29VzfIj1U6/VFv1H6lj2K3Dz6DWmh2fs=" "zip";
-    aarch64-darwin = fetch "apple_universal" "sha256-Cn3/+Dvk5hW9rvxu4I9ghHSS1yWSAeQq3gx+6dvFiIk=" "pkg";
+    aarch64-linux = fetch "linux_arm64" "sha256-fKW2qSQkkC4GcnHcLLszX1pcqK67SaofVX017/cIkD0=" "zip";
+    i686-linux = fetch "linux_386" "sha256-TmQ3nWG12DTpAJaxbK+hnJak0RrFhhw6rJWfV7q8wb4=" "zip";
+    x86_64-linux = fetch "linux_amd64" "sha256-66kFScxPmy4WgK9p1W6qBoAeYJwungHgGkTurjEJy+4=" "zip";
+    aarch64-darwin = fetch "apple_universal" "sha256-DD1j093SjnaPtkQ4XuU1zkRi6XPXtwnBxiqC6wZbV+w=" "pkg";
     x86_64-darwin = aarch64-darwin;
   };
   platforms = builtins.attrNames sources;
diff --git a/pkgs/applications/networking/instant-messengers/element/element-desktop-package.json b/pkgs/applications/networking/instant-messengers/element/element-desktop-package.json
index a244a2ab2a70..46a64d1b533c 100644
--- a/pkgs/applications/networking/instant-messengers/element/element-desktop-package.json
+++ b/pkgs/applications/networking/instant-messengers/element/element-desktop-package.json
@@ -2,7 +2,7 @@
   "name": "element-desktop",
   "productName": "Element",
   "main": "lib/electron-main.js",
-  "version": "1.10.11",
+  "version": "1.10.12",
   "description": "A feature-rich client for Matrix.org",
   "author": "Element",
   "repository": {
@@ -81,11 +81,11 @@
     "rimraf": "^3.0.2",
     "tar": "^6.1.2",
     "ts-node": "^10.4.0",
-    "typescript": "^4.5.3"
+    "typescript": "4.5.5"
   },
   "hakDependencies": {
-    "matrix-seshat": "^2.3.0",
-    "keytar": "^5.6.0"
+    "matrix-seshat": "^2.3.3",
+    "keytar": "^7.9.0"
   },
   "build": {
     "appId": "im.riot.app",
diff --git a/pkgs/applications/networking/instant-messengers/element/pin.json b/pkgs/applications/networking/instant-messengers/element/pin.json
index 70b5f7f65efa..77058ce04c31 100644
--- a/pkgs/applications/networking/instant-messengers/element/pin.json
+++ b/pkgs/applications/networking/instant-messengers/element/pin.json
@@ -1,6 +1,6 @@
 {
-  "version": "1.10.11",
-  "desktopSrcHash": "n74KFmHI6ZQWBEJCR55VZHS//myh2RePcJRVOmZ6XHo=",
-  "desktopYarnHash": "0jm0i1yyfkg1ll11pb3qif1vdxx6rp0yl9kd8jg9nhsg2jzw66pr",
-  "webHash": "02m64bhg1ls4a5igmizkkxnqfmbfhs0xy24ycr75vxmn0zmwa3yd"
+  "version": "1.10.12",
+  "desktopSrcHash": "K1p/+dZRtKb+AiU2EcikAsmiTIKPw0zaVzAfUDzsYZY=",
+  "desktopYarnHash": "09ri87ynfgxrv22sykggiy6nlcf20qwj7zj9qq0rz3c2acr6g9mn",
+  "webHash": "1m7pvliymyggg6qx8gj6l3j2f4rml0km1vmk1zdspxa4l6p0qxd8"
 }
diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix
index c078287b85ee..49b3130a4d9f 100644
--- a/pkgs/applications/science/logic/coq/default.nix
+++ b/pkgs/applications/science/logic/coq/default.nix
@@ -70,9 +70,10 @@ let
       { case = range "8.7" "8.10";  out = ocamlPackages_4_09; }
       { case = range "8.5" "8.6";   out = ocamlPackages_4_05; }
     ] ocamlPackages_4_12;
-  ocamlNativeBuildInputs = [ ocamlPackages.ocaml ocamlPackages.findlib ]
+  ocamlNativeBuildInputs = [ ocamlPackages.ocaml ]
     ++ optional (coqAtLeast "8.14") ocamlPackages.dune_2;
-  ocamlBuildInputs = []
+  ocamlPropagatedNativeBuildInputs = [ ocamlPackages.findlib ];
+  ocamlPropagatedBuildInputs = [ ]
     ++ optional (!coqAtLeast "8.10") ocamlPackages.camlp5
     ++ optional (!coqAtLeast "8.13") ocamlPackages.num
     ++ optional (coqAtLeast "8.13") ocamlPackages.zarith;
@@ -82,7 +83,8 @@ self = stdenv.mkDerivation {
 
   passthru = {
     inherit coq-version;
-    inherit ocamlPackages ocamlBuildInputs ocamlNativeBuildInputs;
+    inherit ocamlPackages ocamlNativeNuildInputs;
+    inherit ocamlPropagatedBuildInputs ocamlPropagatedNativeBuildInputs;
     # For compatibility
     inherit (ocamlPackages) ocaml camlp5 findlib num ;
     emacsBufferSetup = pkgs: ''
@@ -136,13 +138,16 @@ self = stdenv.mkDerivation {
     ++ optional buildIde copyDesktopItems
     ++ optional (buildIde && coqAtLeast "8.10") wrapGAppsHook
     ++ optional (!coqAtLeast "8.6") gnumake42;
-  buildInputs = [ ncurses ] ++ ocamlBuildInputs
+  buildInputs = [ ncurses ]
     ++ optionals buildIde
       (if coqAtLeast "8.10"
        then [ ocamlPackages.lablgtk3-sourceview3 glib gnome.adwaita-icon-theme ]
        else [ ocamlPackages.lablgtk ])
   ;
 
+  propagatedNativeBuildInputs = ocamlPropagatedNativeBuildInputs;
+  propagatedBuildInputs = ocamlPropagatedBuildInputs;
+
   postPatch = ''
     UNAME=$(type -tp uname)
     RM=$(type -tp rm)
diff --git a/pkgs/build-support/coq/default.nix b/pkgs/build-support/coq/default.nix
index a681bbda5575..70c62c659a2d 100644
--- a/pkgs/build-support/coq/default.nix
+++ b/pkgs/build-support/coq/default.nix
@@ -1,4 +1,4 @@
-{ lib, stdenv, coqPackages, coq, fetchzip }@args:
+{ lib, stdenv, coqPackages, coq, which, fetchzip }@args:
 let lib = import ./extra-lib.nix {inherit (args) lib;}; in
 with builtins; with lib;
 let
@@ -15,8 +15,12 @@ in
   releaseRev ? (v: v),
   displayVersion ? {},
   release ? {},
+  buildInputs ? [],
+  nativeBuildInputs ? [],
   extraBuildInputs ? [],
   extraNativeBuildInputs ? [],
+  overrideBuildInputs ? [],
+  overrideNativeBuildInputs ? [],
   namePrefix ? [ "coq" ],
   enableParallelBuilding ? true,
   extraInstallFlags ? [],
@@ -35,7 +39,11 @@ let
   args-to-remove = foldl (flip remove) ([
     "version" "fetcher" "repo" "owner" "domain" "releaseRev"
     "displayVersion" "defaultVersion" "useMelquiondRemake"
-    "release" "extraBuildInputs" "extraNativeBuildInputs" "extraPropagatedBuildInputs" "namePrefix"
+    "release"
+    "buildInputs" "nativeBuildInputs"
+    "extraBuildInputs" "extraNativeBuildInputs"
+    "overrideBuildInputs" "overrideNativeBuildInputs"
+    "namePrefix"
     "meta" "useDune2ifVersion" "useDune2" "opam-name"
     "extraInstallFlags" "setCOQBIN" "mlPlugin"
     "dropAttrs" "dropDerivationAttrs" "keepAttrs" ] ++ dropAttrs) keepAttrs;
@@ -57,9 +65,16 @@ let
     ] "") + optionalString (v == null) "-broken";
   append-version = p: n: p + display-pkg n "" coqPackages.${n}.version + "-";
   prefix-name = foldl append-version "" namePrefix;
-  var-coqlib-install =
-    (optionalString (versions.isGe "8.7" coq.coq-version || coq.coq-version == "dev") "COQMF_") + "COQLIB";
   useDune2 = args.useDune2 or (useDune2ifVersion fetched.version);
+  coqlib-flags = switch coq.coq-version [
+    { case = v: versions.isLe "8.6" v && v != "dev" ;
+      out = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; }
+  ] [ "COQLIBINSTALL=$(out)/lib/coq/${coq.coq-version}/user-contrib"
+      "COQPLUGININSTALL=$(OCAMLFIND_DESTDIR)" ];
+  docdir-flags = switch coq.coq-version [
+    { case = v: versions.isLe "8.6" v && v != "dev";
+      out = [ "DOCDIR=$(out)/share/coq/${coq.coq-version}/" ]; }
+  ] [ "COQDOCINSTALL=$(out)/share/coq/${coq.coq-version}/user-contrib" ];
 in
 
 stdenv.mkDerivation (removeAttrs ({
@@ -68,12 +83,12 @@ stdenv.mkDerivation (removeAttrs ({
 
   inherit (fetched) version src;
 
-  nativeBuildInputs = [ coq ]
-    ++ optionals useDune2 [coq.ocaml coq.ocamlPackages.dune_2]
-    ++ optionals mlPlugin coq.ocamlNativeBuildInputs
-    ++ extraNativeBuildInputs;
-  buildInputs = optionals mlPlugin coq.ocamlBuildInputs
-    ++ extraBuildInputs;
+  nativeBuildInputs = args.overrideNativeBuildInputs
+    or ([ which ] ++ optional useDune2 coq.ocamlPackages.dune_2
+        ++ optional (useDune2 || mlPlugin) coq.ocaml
+        ++ (args.nativeBuildInputs or []) ++ extraNativeBuildInputs);
+  buildInputs = args.overrideBuildInputs
+    or ([ coq ] ++ (args.buildInputs or []) ++ extraBuildInputs);
   inherit enableParallelBuilding;
 
   meta = ({ platforms = coq.meta.platforms; } //
@@ -88,9 +103,7 @@ stdenv.mkDerivation (removeAttrs ({
 // (optionalAttrs setCOQBIN { COQBIN = "${coq}/bin/"; })
 // (optionalAttrs (!args?installPhase && !args?useMelquiondRemake) {
   installFlags =
-    [ "${var-coqlib-install}=$(out)/lib/coq/${coq.coq-version}/" ] ++
-    optional (match ".*doc$" (args.installTargets or "") != null)
-      "DOCDIR=$(out)/share/coq/${coq.coq-version}/" ++
+    [ "DESTDIR=$(out)" ] ++ coqlib-flags ++ docdir-flags ++
     extraInstallFlags;
 })
 // (optionalAttrs useDune2 {
diff --git a/pkgs/development/coq-modules/CoLoR/default.nix b/pkgs/development/coq-modules/CoLoR/default.nix
index 9270609c6b2f..0fdcb49d7300 100644
--- a/pkgs/development/coq-modules/CoLoR/default.nix
+++ b/pkgs/development/coq-modules/CoLoR/default.nix
@@ -20,7 +20,7 @@ with lib; mkCoqDerivation {
   release."1.4.0".rev    = "168c6b86c7d3f87ee51791f795a8828b1521589a";
   release."1.4.0".sha256 = "1d2whsgs3kcg5wgampd6yaqagcpmzhgb6a0hp6qn4lbimck5dfmm";
 
-  extraBuildInputs = [ bignums ];
+  propagatedBuildInputs = [ bignums ];
   enableParallelBuilding = false;
 
   meta = {
diff --git a/pkgs/development/coq-modules/HoTT/default.nix b/pkgs/development/coq-modules/HoTT/default.nix
index 706943cf8d02..f6e9b3daca2d 100644
--- a/pkgs/development/coq-modules/HoTT/default.nix
+++ b/pkgs/development/coq-modules/HoTT/default.nix
@@ -8,7 +8,7 @@ with lib; mkCoqDerivation {
   release."20170921".rev    = "e3557740a699167e6adb1a65855509d55a392fa1";
   release."20170921".sha256 = "0zwfp8g62b50vmmbb2kmskj3v6w7qx1pbf43yw0hr7asdz2zbx5v";
 
-  extraBuildInputs = [ autoconf automake ];
+  nativeBuildInputs = [ autoconf automake ];
 
   preConfigure = ''
     patchShebangs ./autogen.sh
diff --git a/pkgs/development/coq-modules/QuickChick/default.nix b/pkgs/development/coq-modules/QuickChick/default.nix
index db3227c1770e..c2e6a5431c91 100644
--- a/pkgs/development/coq-modules/QuickChick/default.nix
+++ b/pkgs/development/coq-modules/QuickChick/default.nix
@@ -36,8 +36,7 @@ let recent = lib.versions.isGe "8.7" coq.coq-version; in
     "substituteInPlace Makefile --replace quickChickTool.byte quickChickTool.native";
 
   mlPlugin = true;
-  extraNativeBuildInputs = lib.optional recent coq.ocamlPackages.ocamlbuild;
-  extraBuildInputs = lib.optional recent coq.ocamlPackages.num;
+  nativeBuildInputs = lib.optional recent coq.ocamlPackages.ocamlbuild;
   propagatedBuildInputs = [ ssreflect ]
     ++ lib.optionals recent [ coq-ext-lib simple-io ];
   extraInstallFlags = [ "-f Makefile.coq" ];
diff --git a/pkgs/development/coq-modules/VST/default.nix b/pkgs/development/coq-modules/VST/default.nix
index a5dee94d045d..8bf8a8680237 100644
--- a/pkgs/development/coq-modules/VST/default.nix
+++ b/pkgs/development/coq-modules/VST/default.nix
@@ -31,7 +31,7 @@ mkCoqDerivation {
   release."2.9".sha256 = "sha256:1adwzbl1pprrrwrm7cm493098fizxanxpv7nyfbvwdhgbhcnv6qf";
   release."2.8".sha256 = "sha256-cyK88uzorRfjapNQ6XgQEmlbWnDsiyLve5po1VG52q0=";
   releaseRev = v: "v${v}";
-  extraBuildInputs = [ ITree ];
+  buildInputs = [ ITree ];
   propagatedBuildInputs = [ compcert ];
 
   preConfigure = ''
diff --git a/pkgs/development/coq-modules/bignums/default.nix b/pkgs/development/coq-modules/bignums/default.nix
index 0001ae1ded4d..a53b8199fe96 100644
--- a/pkgs/development/coq-modules/bignums/default.nix
+++ b/pkgs/development/coq-modules/bignums/default.nix
@@ -5,7 +5,7 @@ with lib; mkCoqDerivation {
   owner = "coq";
   displayVersion = { bignums = ""; };
   inherit version;
-  defaultVersion = if versions.isGe "8.5" coq.coq-version
+  defaultVersion = if versions.isGe "8.6" coq.coq-version
     then "${coq.coq-version}.0" else null;
 
   release."8.15.0".sha256 = "093klwlhclgyrba1iv18dyz1qp5f0lwiaa7y0qwvgmai8rll5fns";
diff --git a/pkgs/development/coq-modules/compcert/default.nix b/pkgs/development/coq-modules/compcert/default.nix
index 092bb58d174f..5d2eb4433e6b 100644
--- a/pkgs/development/coq-modules/compcert/default.nix
+++ b/pkgs/development/coq-modules/compcert/default.nix
@@ -1,5 +1,5 @@
 { lib, fetchzip, mkCoqDerivation, coq, flocq, compcert
-, ocamlPackages, fetchpatch, makeWrapper, coq2html
+, fetchpatch, makeWrapper, coq2html
 , stdenv, tools ? stdenv.cc
 , version ? null
 }:
@@ -15,9 +15,9 @@ let compcert = mkCoqDerivation rec {
   releaseRev = v: "v${v}";
 
   defaultVersion =  with versions; switch coq.version [
-      { case = range "8.8" "8.11"; out = "3.8"; }
+      { case = range "8.13" "8.15"; out = "3.10"; }
       { case = isEq "8.12"       ; out = "3.9"; }
-      { case = range "8.12" "8.15"; out = "3.10"; }
+      { case = range "8.8" "8.11"; out = "3.8"; }
     ] null;
 
   release = {
@@ -26,8 +26,9 @@ let compcert = mkCoqDerivation rec {
     "3.10".sha256 = "sha256:19rmx8r8v46101ij5myfrz60arqjy7q3ra3fb8mxqqi3c8c4l4j6";
   };
 
+  mlPlugin = true;
   nativeBuildInputs = [ makeWrapper ];
-  buildInputs = with ocamlPackages; [ ocaml findlib menhir menhirLib ] ++ [ coq coq2html ];
+  buildInputs = with coq.ocamlPackages; [ menhir menhirLib ] ++ [ coq2html ];
   propagatedBuildInputs = [ flocq ];
 
   enableParallelBuilding = true;
@@ -48,9 +49,13 @@ let compcert = mkCoqDerivation rec {
   '';
 
   installTargets = "documentation install";
+  installFlags = []; # trust ./configure
+  preInstall = ''
+    mkdir -p $out/share/man
+    mkdir -p $man/share
+  '';
   postInstall = ''
     # move man into place
-    mkdir -p $man/share
     mv $out/share/man/ $man/share/
 
     # move docs into place
diff --git a/pkgs/development/coq-modules/coq-bits/default.nix b/pkgs/development/coq-modules/coq-bits/default.nix
index 6cb6bb3c813e..f604db4ecdf7 100644
--- a/pkgs/development/coq-modules/coq-bits/default.nix
+++ b/pkgs/development/coq-modules/coq-bits/default.nix
@@ -1,34 +1,18 @@
-{ lib, mkCoqDerivation, coq, mathcomp, version ? null }:
+{ lib, mkCoqDerivation, coq, mathcomp-algebra, version ? null }:
 
 with lib; mkCoqDerivation {
   pname = "coq-bits";
   repo = "bits";
   inherit version;
-  defaultVersion =
-    if versions.isGe "8.10" coq.version
-    then "1.1.0"
-    else if versions.isGe "8.7" coq.version
-    then "1.0.0"
-    else null;
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = isGe "8.10"; out = "1.1.0"; }
+    { case = isGe "8.7";  out = "1.0.0"; }
+  ] null;
 
-  release = {
-    "1.0.0" = {
-      rev = "1.0.0";
-      sha256 = "0nv5mdgrd075dpd8bc7h0xc5i95v0pkm0bfyq5rj6ii1s54dwcjl";
-    };
-    "1.1.0" = {
-      rev = "1.1.0";
-      sha256 = "sha256-TCw1kSXeW0ysIdLeNr+EGmpGumEE9i8tinEMp57UXaE=";
-    };
-  };
+  release."1.1.0".sha256 = "sha256-TCw1kSXeW0ysIdLeNr+EGmpGumEE9i8tinEMp57UXaE=";
+  release."1.0.0".sha256 = "0nv5mdgrd075dpd8bc7h0xc5i95v0pkm0bfyq5rj6ii1s54dwcjl";
 
-  extraBuildInputs = [ mathcomp.ssreflect mathcomp.fingroup ];
-  propagatedBuildInputs = [ mathcomp.algebra ];
-
-  installPhase = ''
-    make -f Makefile CoqMakefile
-    make -f CoqMakefile COQLIB=$out/lib/coq/${coq.coq-version}/ install
-  '';
+  propagatedBuildInputs = [ mathcomp-algebra ];
 
   meta = {
     description = "A formalization of bitset operations in Coq";
diff --git a/pkgs/development/coq-modules/coq-elpi/default.nix b/pkgs/development/coq-modules/coq-elpi/default.nix
index 55423047caa7..03fe8c32d5c3 100644
--- a/pkgs/development/coq-modules/coq-elpi/default.nix
+++ b/pkgs/development/coq-modules/coq-elpi/default.nix
@@ -7,7 +7,7 @@ with builtins; with lib; let
     { case = "8.13"; out = { version = "1.13.7"; };}
     { case = "8.14"; out = { version = "1.13.7"; };}
     { case = "8.15"; out = { version = "1.14.1"; };}
-  ] {});
+  ] { version = "1.14.1"; } );
 in mkCoqDerivation {
   pname = "elpi";
   repo  = "coq-elpi";
@@ -48,8 +48,8 @@ in mkCoqDerivation {
   release."1.6.0".sha256      = "0kf99i43mlf750fr7fric764mm495a53mg5kahnbp6zcjcxxrm0b";
   releaseRev = v: "v${v}";
 
-  extraNativeBuildInputs = [ which elpi ];
   mlPlugin = true;
+  propagatedBuildInputs = [ elpi ];
 
   meta = {
     description = "Coq plugin embedding ELPI.";
diff --git a/pkgs/development/coq-modules/coqeal/default.nix b/pkgs/development/coq-modules/coqeal/default.nix
index 3b8b23618d23..563e2dc22d6d 100644
--- a/pkgs/development/coq-modules/coqeal/default.nix
+++ b/pkgs/development/coq-modules/coqeal/default.nix
@@ -1,6 +1,6 @@
 { coq, mkCoqDerivation, mathcomp, bignums, paramcoq, multinomials,
   mathcomp-real-closed,
-  lib, which, version ? null }:
+  lib, version ? null }:
 
 with lib;
 
@@ -22,7 +22,6 @@ with lib;
   release."1.0.4".sha256 = "1g5m26lr2lwxh6ld2gykailhay4d0ayql4bfh0aiwqpmmczmxipk";
   release."1.0.3".sha256 = "0hc63ny7phzbihy8l7wxjvn3haxx8jfnhi91iw8hkq8n29i23v24";
 
-  extraBuildInputs = [ which ];
   propagatedBuildInputs = [ mathcomp.algebra bignums paramcoq multinomials ];
 
   meta = {
diff --git a/pkgs/development/coq-modules/coqhammer/default.nix b/pkgs/development/coq-modules/coqhammer/default.nix
index 66a3dd222dd5..853e77990b6e 100644
--- a/pkgs/development/coq-modules/coqhammer/default.nix
+++ b/pkgs/development/coq-modules/coqhammer/default.nix
@@ -28,8 +28,10 @@ with lib; mkCoqDerivation {
   release."1.3-coq8.12".sha256   = "1q1y3cwhd98pkm98g71fsdjz85bfwgcz2xn7s7wwmiraifv5l6z8";
   release."1.3-coq8.11".sha256   = "08zf8qfna7b9p2myfaz4g7bas3a1q1156x78n5isqivlnqfrjc1b";
   release."1.3-coq8.10".sha256   = "1fj8497ir4m79hyrmmmmrag01001wrby0h24wv6525vz0w5py3cd";
-  release."1.1.1-coq8.9".sha256  = "1knjmz4hr8vlp103j8n4fyb2lfxysnm512gh3m2kp85n6as6fvb9";
-  release."1.1-coq8.8".sha256    = "0ms086wp4jmrzyglb8wymchzyflflk01nsfsk4r6qv8rrx81nx9h";
+  release."1.1.1-coq8.9" = { sha256 = "1knjmz4hr8vlp103j8n4fyb2lfxysnm512gh3m2kp85n6as6fvb9";
+                             rev    = "f8b4d81a213aa1f25afbe53c7c9ca1b15e3d42bc"; };
+  release."1.1-coq8.8" =   { sha256 = "0ms086wp4jmrzyglb8wymchzyflflk01nsfsk4r6qv8rrx81nx9h";
+                             rev    = "c3cb54b4d5f33fab372d33c7189861368a08fa22"; };
 
   release."1.3.1-coq8.13".version  = "1.3.1";
   release."1.3.1-coq8.12".version  = "1.3.1";
diff --git a/pkgs/development/coq-modules/coqprime/default.nix b/pkgs/development/coq-modules/coqprime/default.nix
index 46ede02a57e6..26988b81e1a6 100644
--- a/pkgs/development/coq-modules/coqprime/default.nix
+++ b/pkgs/development/coq-modules/coqprime/default.nix
@@ -20,7 +20,6 @@ with lib; mkCoqDerivation {
   release."8.7.2".sha256 = "15zlcrx06qqxjy3nhh22wzy0rb4npc8l4nx2bbsfsvrisbq1qb7k";
   releaseRev = v: "v${v}";
 
-  extraBuildInputs = [ which ];
   propagatedBuildInputs = [ bignums ];
 
   meta = with lib; {
diff --git a/pkgs/development/coq-modules/coqtail-math/default.nix b/pkgs/development/coq-modules/coqtail-math/default.nix
index 3491e6b21f2f..a4f7ca405f71 100644
--- a/pkgs/development/coq-modules/coqtail-math/default.nix
+++ b/pkgs/development/coq-modules/coqtail-math/default.nix
@@ -14,9 +14,7 @@ mkCoqDerivation {
   release."8.14".sha256 = "sha256:1k8f8idjnx0mf4z479vcx55iz42rjxrbplbznv80m2famxakq03c";
   release."20201124".rev    = "5c22c3d7dcd8cf4c47cf84a281780f5915488e9e";
   release."20201124".sha256 = "sha256-wd+Lh7dpAD4zfpyKuztDmSFEZo5ZiFrR8ti2jUCVvoQ=";
-
-  extraNativeBuildInputs = with coq.ocamlPackages; [ ocaml findlib ];
-
+  mlPlugin = true;
   meta = {
     license = licenses.lgpl3Only;
     maintainers = [ maintainers.siraben ];
diff --git a/pkgs/development/coq-modules/coquelicot/default.nix b/pkgs/development/coq-modules/coquelicot/default.nix
index 1a6dba9b0c08..09dd65df41d2 100644
--- a/pkgs/development/coq-modules/coquelicot/default.nix
+++ b/pkgs/development/coq-modules/coquelicot/default.nix
@@ -1,4 +1,4 @@
-{ lib, mkCoqDerivation, which, autoconf,
+{ lib, mkCoqDerivation, autoconf,
   coq, ssreflect, version ? null }:
 
 with lib; mkCoqDerivation {
@@ -16,7 +16,7 @@ with lib; mkCoqDerivation {
   release."3.0.2".sha256 = "1rqfbbskgz7b1bcpva8wh3v3456sq2364y804f94sc8y5sij23nl";
   releaseRev = v: "coquelicot-${v}";
 
-  extraNativeBuildInputs = [ which autoconf ];
+  nativeBuildInputs = [ autoconf ];
   propagatedBuildInputs = [ ssreflect ];
   useMelquiondRemake.logpath = "Coquelicot";
 
diff --git a/pkgs/development/coq-modules/dpdgraph/default.nix b/pkgs/development/coq-modules/dpdgraph/default.nix
index 7cf6132bf6a9..fcc1303e8276 100644
--- a/pkgs/development/coq-modules/dpdgraph/default.nix
+++ b/pkgs/development/coq-modules/dpdgraph/default.nix
@@ -39,9 +39,9 @@ mkCoqDerivation {
   release."0.6".sha256   = "0qvar8gfbrcs9fmvkph5asqz4l5fi63caykx3bsn8zf0xllkwv0n";
   releaseRev = v: "v${v}";
 
-  extraNativeBuildInputs = [ autoreconfHook ];
+  nativeBuildInputs = [ autoreconfHook ];
   mlPlugin = true;
-  extraBuildInputs = [ coq.ocamlPackages.ocamlgraph ];
+  buildInputs = [ coq.ocamlPackages.ocamlgraph ];
 
   # dpd_compute.ml uses deprecated Pervasives.compare
   # Versions prior to 0.6.5 do not have the WARN_ERR build flag
diff --git a/pkgs/development/coq-modules/fiat/HEAD.nix b/pkgs/development/coq-modules/fiat/HEAD.nix
index 47f097a34b2e..d94dc03b6377 100644
--- a/pkgs/development/coq-modules/fiat/HEAD.nix
+++ b/pkgs/development/coq-modules/fiat/HEAD.nix
@@ -8,10 +8,10 @@ with lib; mkCoqDerivation rec {
   inherit version;
   defaultVersion = if coq.coq-version == "8.5" then "2016-10-24" else null;
   release."2016-10-24".rev    = "7feb6c64be9ebcc05924ec58fe1463e73ec8206a";
-  release."2016-10-24".sha256 = "0griqc675yylf9rvadlfsabz41qy5f5idya30p5rv6ysiakxya64";
+  release."2016-10-24".sha256 = "16y57vibq3f5i5avgj80f4i3aw46wdwzx36k5d3pf3qk17qrlrdi";
 
   mlPlugin = true;
-  extraBuildInputs = [ python27 ];
+  buildInputs = [ python27 ];
 
   prePatch = "patchShebangs etc/coq-scripts";
 
diff --git a/pkgs/development/coq-modules/flocq/default.nix b/pkgs/development/coq-modules/flocq/default.nix
index f13aec883e76..a0f4a3ecae82 100644
--- a/pkgs/development/coq-modules/flocq/default.nix
+++ b/pkgs/development/coq-modules/flocq/default.nix
@@ -1,4 +1,4 @@
-{ lib, which, autoconf, automake,
+{ lib, bash, autoconf, automake,
   mkCoqDerivation, coq, version ? null }:
 
 with lib; mkCoqDerivation {
@@ -16,7 +16,7 @@ with lib; mkCoqDerivation {
   release."2.6.1".sha256 = "0q5a038ww5dn72yvwn5298d3ridkcngb1dik8hdyr3xh7gr5qibj";
   releaseRev = v: "flocq-${v}";
 
-  nativeBuildInputs = [ which autoconf ];
+  nativeBuildInputs = [ bash autoconf ];
   mlPlugin = true;
   useMelquiondRemake.logpath = "Flocq";
 
diff --git a/pkgs/development/coq-modules/gappalib/default.nix b/pkgs/development/coq-modules/gappalib/default.nix
index 23cbd46743b1..903b3518e5d6 100644
--- a/pkgs/development/coq-modules/gappalib/default.nix
+++ b/pkgs/development/coq-modules/gappalib/default.nix
@@ -13,7 +13,7 @@ with lib; mkCoqDerivation {
   release."1.4.4".sha256 = "114q2hgw64j6kqa9mg3qcp1nlf0ia46z2xadq81fnkxqm856ml7l";
   releaseRev = v: "gappalib-coq-${v}";
 
-  extraNativeBuildInputs = [ which autoconf ];
+  nativeBuildInputs = [ autoconf ];
   mlPlugin = true;
   propagatedBuildInputs = [ flocq ];
   useMelquiondRemake.logpath = "Gappa";
diff --git a/pkgs/development/coq-modules/heq/default.nix b/pkgs/development/coq-modules/heq/default.nix
index 4bf9139b4947..c3a815eb5c87 100644
--- a/pkgs/development/coq-modules/heq/default.nix
+++ b/pkgs/development/coq-modules/heq/default.nix
@@ -1,22 +1,26 @@
 {lib, fetchzip, mkCoqDerivation, coq, version ? null }:
 
+let fetcher = {rev, repo, owner, sha256, domain, ...}:
+  fetchzip {
+    url = "https://${domain}/${owner}/${repo}/download/${repo}-${rev}.zip";
+    inherit sha256;
+   }; in
 with lib; mkCoqDerivation {
   pname = "heq";
   repo = "Heq";
-  owner = "gil";
-  domain = "mpi-sws.org";
+  owner = "gil.hur";
+  domain = "sf.snu.ac.kr";
   inherit version fetcher;
   defaultVersion = if versions.isLt "8.8" coq.coq-version then "0.92" else null;
   release."0.92".sha256 = "0cf8y6728n81wwlbpq3vi7l2dbzi7759klypld4gpsjjp1y1fj74";
 
   mlPlugin = true;
-  propagatedBuildInputs = [ coq ];
-
-  extraInstallFlags = [ "COQLIB=$out/lib/coq/${coq.coq-version}" ];
   preBuild = "cd src";
 
+  extraInstallFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ];
+
   meta = {
-    homepage = "https://www.mpi-sws.org/~gil/Heq/";
+    homepage = "https://ropas.snu.ac.kr/~gil.hur/Heq/";
     description = "Heq : a Coq library for Heterogeneous Equality";
     maintainers = with maintainers; [ jwiegley ];
   };
diff --git a/pkgs/development/coq-modules/hierarchy-builder/default.nix b/pkgs/development/coq-modules/hierarchy-builder/default.nix
index c0fa2d7c8e00..6f15fc80388e 100644
--- a/pkgs/development/coq-modules/hierarchy-builder/default.nix
+++ b/pkgs/development/coq-modules/hierarchy-builder/default.nix
@@ -1,4 +1,4 @@
-{ lib, mkCoqDerivation, which, coq, coq-elpi, version ? null }:
+{ lib, mkCoqDerivation, coq, coq-elpi, version ? null }:
 
 with lib; let hb = mkCoqDerivation {
   pname = "hierarchy-builder";
@@ -17,13 +17,10 @@ with lib; let hb = mkCoqDerivation {
   release."0.10.0".sha256 = "1a3vry9nzavrlrdlq3cys3f8kpq3bz447q8c4c7lh2qal61wb32h";
   releaseRev = v: "v${v}";
 
-  extraNativeBuildInputs = [ which ];
-
   propagatedBuildInputs = [ coq-elpi ];
 
   mlPlugin = true;
 
-  installFlags = [ "DESTDIR=$(out)" "COQMF_COQLIB=lib/coq/${coq.coq-version}" ];
   extraInstallFlags = [ "VFILES=structures.v" ];
 
   meta = {
diff --git a/pkgs/development/coq-modules/interval/default.nix b/pkgs/development/coq-modules/interval/default.nix
index b9257d415e57..4134a8fd573d 100644
--- a/pkgs/development/coq-modules/interval/default.nix
+++ b/pkgs/development/coq-modules/interval/default.nix
@@ -1,4 +1,5 @@
-{ lib, mkCoqDerivation, which, autoconf, coq, coquelicot, flocq, mathcomp-ssreflect, mathcomp-fingroup, bignums ? null, gnuplot_qt, version ? null }:
+{ lib, mkCoqDerivation, autoconf, coq, coquelicot, flocq,
+  mathcomp-ssreflect, mathcomp-fingroup, bignums ? null, gnuplot_qt, version ? null }:
 
 mkCoqDerivation rec {
   pname = "interval";
@@ -20,8 +21,9 @@ mkCoqDerivation rec {
   release."3.3.0".sha256 = "0lz2hgggzn4cvklvm8rpaxvwaryf37i8mzqajqgdxdbd8f12acsz";
   releaseRev = v: "interval-${v}";
 
-  extraNativeBuildInputs = [ which autoconf ];
-  propagatedBuildInputs = [ bignums coquelicot flocq mathcomp-ssreflect mathcomp-fingroup ]
+  nativeBuildInputs = [ autoconf ];
+  propagatedBuildInputs = lib.optional (lib.versions.isGe "8.6" coq.coq-version) bignums
+    ++ [ coquelicot flocq mathcomp-ssreflect mathcomp-fingroup ]
     ++ lib.optionals (lib.versions.isGe "4.2.0" defaultVersion) [ gnuplot_qt ];
   useMelquiondRemake.logpath = "Interval";
   mlPlugin = true;
diff --git a/pkgs/development/coq-modules/itauto/default.nix b/pkgs/development/coq-modules/itauto/default.nix
index 4993a76b4f08..151a0511c806 100644
--- a/pkgs/development/coq-modules/itauto/default.nix
+++ b/pkgs/development/coq-modules/itauto/default.nix
@@ -17,7 +17,7 @@ mkCoqDerivation rec {
   ] null;
 
   mlPlugin = true;
-  extraNativeBuildInputs = (with coq.ocamlPackages; [ ocamlbuild ]);
+  nativeBuildInputs = (with coq.ocamlPackages; [ ocamlbuild ]);
   enableParallelBuilding = false;
 
   meta = {
diff --git a/pkgs/development/coq-modules/ltac2/default.nix b/pkgs/development/coq-modules/ltac2/default.nix
index 1d0d03fb7f7c..c938a7ad0279 100644
--- a/pkgs/development/coq-modules/ltac2/default.nix
+++ b/pkgs/development/coq-modules/ltac2/default.nix
@@ -17,7 +17,6 @@ with lib; mkCoqDerivation {
   release."0.1-8.7".rev     = "v0.1-8.7";
   release."0.1-8.7".sha256  = "0l6wiwi4cvd0i324fb29i9mdh0ijlxzggw4mrjjy695l2qdnlgg0";
 
-  nativeBuildInputs = [ which ];
   mlPlugin = true;
 
   meta = {
diff --git a/pkgs/development/coq-modules/math-classes/default.nix b/pkgs/development/coq-modules/math-classes/default.nix
index 0a78191d8b72..2504e852bafd 100644
--- a/pkgs/development/coq-modules/math-classes/default.nix
+++ b/pkgs/development/coq-modules/math-classes/default.nix
@@ -9,7 +9,7 @@ with lib; mkCoqDerivation {
   release."8.13.0".sha256 = "1ln7ziivfbxzbdvlhbvyg3v30jgblncmwcsam6gg3d1zz6r7cbby";
   release."8.15.0".sha256 = "10w1hm537k6jx8a8vghq1yx12rsa0sjk2ipv3scgir71ln30hllw";
 
-  extraBuildInputs = [ bignums ];
+  propagatedBuildInputs = [ bignums ];
 
   meta = {
     homepage = "https://math-classes.github.io";
diff --git a/pkgs/development/coq-modules/mathcomp/default.nix b/pkgs/development/coq-modules/mathcomp/default.nix
index 0f562fec287c..a19d8b8dcc79 100644
--- a/pkgs/development/coq-modules/mathcomp/default.nix
+++ b/pkgs/development/coq-modules/mathcomp/default.nix
@@ -10,9 +10,9 @@
 # See the documentation at doc/languages-frameworks/coq.section.md.        #
 ############################################################################
 
-{ lib, ncurses, which, graphviz, lua, fetchzip,
+{ lib, ncurses, graphviz, lua, fetchzip,
   mkCoqDerivation, recurseIntoAttrs, withDoc ? false, single ? false,
-  coqPackages, coq, ocamlPackages, version ? null }@args:
+  coqPackages, coq, version ? null }@args:
 with builtins // lib;
 let
   repo  = "math-comp";
@@ -60,8 +60,9 @@ let
         inherit version pname defaultVersion release releaseRev repo owner;
 
         mlPlugin = versions.isLe "8.6" coq.coq-version;
-        extraNativeBuildInputs = [ which ] ++ optionals withDoc [ graphviz lua ];
-        extraBuildInputs = [ ncurses ] ++ mathcomp-deps;
+        nativeBuildInputs = optionals withDoc [ graphviz lua ];
+        buildInputs = [ ncurses ];
+        propagatedBuildInputs = mathcomp-deps;
 
         buildFlags = optional withDoc "doc";
 
diff --git a/pkgs/development/coq-modules/metacoq/default.nix b/pkgs/development/coq-modules/metacoq/default.nix
index 583d8b7adb91..09327f46b86d 100644
--- a/pkgs/development/coq-modules/metacoq/default.nix
+++ b/pkgs/development/coq-modules/metacoq/default.nix
@@ -1,4 +1,4 @@
-{ lib, which, fetchzip,
+{ lib, fetchzip,
   mkCoqDerivation, recurseIntoAttrs,  single ? false,
   coqPackages, coq, equations, version ? null }@args:
 with builtins // lib;
@@ -36,10 +36,8 @@ let
       derivation = mkCoqDerivation ({
         inherit version pname defaultVersion release releaseRev repo owner;
 
-        extraNativeBuildInputs = [ which ];
         mlPlugin = true;
-        extraBuildInputs = [ coq.ocamlPackages.zarith ];
-        propagatedBuildInputs = [ equations ] ++ metacoq-deps;
+        propagatedBuildInputs = [ equations coq.ocamlPackages.zarith ] ++ metacoq-deps;
 
         patchPhase =  ''
           patchShebangs ./configure.sh
diff --git a/pkgs/development/coq-modules/metalib/default.nix b/pkgs/development/coq-modules/metalib/default.nix
index 26bd38f72df1..83333b3e1bf0 100644
--- a/pkgs/development/coq-modules/metalib/default.nix
+++ b/pkgs/development/coq-modules/metalib/default.nix
@@ -13,7 +13,6 @@ with lib; mkCoqDerivation {
   release."8.10".sha256 = "0wbypc05d2lqfm9qaw98ynr5yc1p0ipsvyc3bh1rk9nz7zwirmjs";
 
   sourceRoot = "source/Metalib";
-  installFlags = "COQMF_COQLIB=$(out)/lib/coq/${coq.coq-version}";
 
   meta = {
     license = licenses.mit;
diff --git a/pkgs/development/coq-modules/semantics/default.nix b/pkgs/development/coq-modules/semantics/default.nix
index e112512ec5c7..cbf1469e1f03 100644
--- a/pkgs/development/coq-modules/semantics/default.nix
+++ b/pkgs/development/coq-modules/semantics/default.nix
@@ -24,8 +24,8 @@ mkCoqDerivation rec {
   ] null;
 
   mlPlugin = true;
-  extraNativeBuildInputs = (with coq.ocamlPackages; [ ocamlbuild ]);
-  extraBuildInputs = (with coq.ocamlPackages; [ num ]);
+  nativeBuildInputs = (with coq.ocamlPackages; [ ocamlbuild ]);
+  propagatedBuildInputs = (with coq.ocamlPackages; [ num ]);
 
   postPatch = ''
     for p in Make Makefile.coq.local
diff --git a/pkgs/development/coq-modules/simple-io/default.nix b/pkgs/development/coq-modules/simple-io/default.nix
index bcc391c4f724..ca7325711e25 100644
--- a/pkgs/development/coq-modules/simple-io/default.nix
+++ b/pkgs/development/coq-modules/simple-io/default.nix
@@ -11,11 +11,9 @@ with lib; mkCoqDerivation {
   ] null;
   release."1.7.0".sha256 = "sha256:1a1q9x2abx71hqvjdai3n12jxzd49mhf3nqqh3ya2ssl2lj609ci";
   release."1.3.0".sha256 = "1yp7ca36jyl9kz35ghxig45x6cd0bny2bpmy058359p94wc617ax";
-  extraNativeBuildInputs = (with coq.ocamlPackages; [ cppo zarith ]);
-  propagatedBuildInputs = [ coq-ext-lib ]
-  ++ (with coq.ocamlPackages; [ ocaml ocamlbuild ]);
-
   mlPlugin = true;
+  nativeBuildInputs = [ coq.ocamlPackages.cppo ];
+  propagatedBuildInputs = [ coq-ext-lib coq.ocamlPackages.ocamlbuild ];
 
   doCheck = true;
   checkTarget = "test";
diff --git a/pkgs/development/coq-modules/smtcoq/default.nix b/pkgs/development/coq-modules/smtcoq/default.nix
index 0389b45fb5cd..ebaebe6974e3 100644
--- a/pkgs/development/coq-modules/smtcoq/default.nix
+++ b/pkgs/development/coq-modules/smtcoq/default.nix
@@ -13,9 +13,11 @@ mkCoqDerivation {
     { case = isEq "8.13"; out = "itp22"; }
   ] null;
 
-  propagatedBuildInputs = [ trakt cvc4 ] ++ lib.optionals (!stdenv.isDarwin) [ veriT ];
-  extraNativeBuildInputs = with coq.ocamlPackages; [ ocaml ocamlbuild ];
-  extraBuildInputs = with coq.ocamlPackages; [ findlib num zarith ];
+  propagatedBuildInputs = [ trakt cvc4 ]
+    ++ lib.optionals (!stdenv.isDarwin) [ veriT ]
+    ++ (with coq.ocamlPackages; [ num zarith ]);
+  mlPlugin = true;
+  nativeBuildInputs = with coq.ocamlPackages; [ ocamlbuild ];
 
   meta = {
     description = "Communication between Coq and SAT/SMT solvers ";
diff --git a/pkgs/development/ocaml-modules/elpi/default.nix b/pkgs/development/ocaml-modules/elpi/default.nix
index 0770f3a48d48..cc8428425177 100644
--- a/pkgs/development/ocaml-modules/elpi/default.nix
+++ b/pkgs/development/ocaml-modules/elpi/default.nix
@@ -1,12 +1,13 @@
-{ stdenv, lib, fetchzip, buildDunePackage, camlp5
+{ stdenv, lib, fetchzip, bash
+, buildDunePackage, camlp5
 , re, perl, ncurses
 , ppxlib, ppx_deriving
 , ppxlib_0_15, ppx_deriving_0_15
+, coqPackages
 , version ? "1.14.1"
 }:
 with lib;
-let fetched = import ../../../build-support/coq/meta-fetch/default.nix
-  {inherit lib stdenv fetchzip; } ({
+let fetched = coqPackages.metaFetch ({
     release."1.14.1".sha256 = "sha256-BZPVL8ymjrE9kVGyf6bpc+GA2spS5JBpkUtZi04nPis=";
     release."1.13.7".sha256 = "10fnwz30bsvj7ii1vg4l1li5pd7n0qqmwj18snkdr5j9gk0apc1r";
     release."1.13.5".sha256 = "02a6r23mximrdvs6kgv6rp0r2dgk7zynbs99nn7lphw2c4189kka";
@@ -32,6 +33,11 @@ buildDunePackage rec {
      else [ ppxlib_0_15 ppx_deriving_0_15 ]
   );
 
+  patchPhase = ''
+    sed -e "s/SHELL:=/SHELL?=/" -i Makefile || true
+  '';
+  buildPhase = "SHELL=${bash} make build";
+
   meta = {
     description = "Embeddable λProlog Interpreter";
     license = licenses.lgpl21Plus;
diff --git a/pkgs/development/python-modules/mapbox/default.nix b/pkgs/development/python-modules/mapbox/default.nix
index f721228ddca4..84ca6199e2f4 100644
--- a/pkgs/development/python-modules/mapbox/default.nix
+++ b/pkgs/development/python-modules/mapbox/default.nix
@@ -32,5 +32,8 @@ buildPythonPackage rec {
     description = "Mapbox SDK for Python";
     longDescription = "Low-level client API for Mapbox web services.";
     maintainers = with maintainers; [ ersin ];
+    # ImportError: cannot import name 'Mapping' from 'collections'
+    # and archived upstreamed
+    broken = true;
   };
 }
diff --git a/pkgs/development/python-modules/napalm/default.nix b/pkgs/development/python-modules/napalm/default.nix
index 2266283cc53b..ef59a33a956a 100644
--- a/pkgs/development/python-modules/napalm/default.nix
+++ b/pkgs/development/python-modules/napalm/default.nix
@@ -1,10 +1,14 @@
 { lib, buildPythonPackage, fetchFromGitHub, callPackage, setuptools, cffi
 , paramiko, requests, future, textfsm, jinja2, netaddr, pyyaml, pyeapi, netmiko
-, junos-eznc, ciscoconfparse, scp, lxml, ncclient, pytestCheckHook, ddt, mock }:
+, junos-eznc, ciscoconfparse, scp, lxml, ncclient, pytestCheckHook, ddt, mock
+, pythonOlder, pythonAtLeast }:
 
 buildPythonPackage rec {
   pname = "napalm";
   version = "3.3.1";
+  format = "setuptools";
+
+  disabled = pythonOlder "3.6" || pythonAtLeast "3.9";
 
   src = fetchFromGitHub {
     owner = "napalm-automation";
diff --git a/pkgs/development/python-modules/nose/default.nix b/pkgs/development/python-modules/nose/default.nix
index 586af7a90423..31fd824ee3da 100644
--- a/pkgs/development/python-modules/nose/default.nix
+++ b/pkgs/development/python-modules/nose/default.nix
@@ -41,8 +41,8 @@ buildPythonPackage rec {
 
   meta = with lib; {
     description = "A unittest-based testing framework for python that makes writing and running tests easier";
-    homepage = "http://readthedocs.org/docs/nose/";
+    homepage = "https://nose.readthedocs.io/";
     license = licenses.lgpl3;
+    maintainers = with maintainers; [ ];
   };
-
 }
diff --git a/pkgs/development/python-modules/scikit-bio/default.nix b/pkgs/development/python-modules/scikit-bio/default.nix
index d2c32fc138af..e86b384f9c4a 100644
--- a/pkgs/development/python-modules/scikit-bio/default.nix
+++ b/pkgs/development/python-modules/scikit-bio/default.nix
@@ -5,6 +5,7 @@
 , lockfile
 , cachecontrol
 , decorator
+, h5py
 , ipython
 , matplotlib
 , natsort
@@ -19,18 +20,18 @@
 }:
 
 buildPythonPackage rec {
-  version = "0.5.6";
+  version = "0.5.7";
   pname = "scikit-bio";
   disabled = !isPy3k;
 
   src = fetchPypi {
     inherit pname version;
-    sha256 = "48b73ec53ce0ff2c2e3e05f3cfcf93527c1525a8d3e9dd4ae317b4219c37f0ea";
+    sha256 = "sha256-Y0PKDGIeL8xdHAQsi+MgBmTFMllWqDvqdRzxvMddHak=";
   };
 
-  buildInputs = [ cython ];
+  nativeBuildInputs = [ cython ];
   checkInputs = [ coverage ];
-  propagatedBuildInputs = [ lockfile cachecontrol decorator ipython matplotlib natsort numpy pandas scipy hdmedians scikit-learn ];
+  propagatedBuildInputs = [ lockfile cachecontrol decorator ipython matplotlib natsort numpy pandas scipy h5py hdmedians scikit-learn ];
 
   # cython package not included for tests
   doCheck = false;
diff --git a/pkgs/development/tools/parsing/tree-sitter/default.nix b/pkgs/development/tools/parsing/tree-sitter/default.nix
index e3d74600c955..441dc4988f52 100644
--- a/pkgs/development/tools/parsing/tree-sitter/default.nix
+++ b/pkgs/development/tools/parsing/tree-sitter/default.nix
@@ -166,6 +166,6 @@ rustPlatform.buildRustPackage {
       * Dependency-free so that the runtime library (which is written in pure C) can be embedded in any application
     '';
     license = licenses.mit;
-    maintainers = with maintainers; [ Profpatsch ];
+    maintainers = with maintainers; [ Profpatsch oxalica ];
   };
 }
diff --git a/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-c-sharp.json b/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-c-sharp.json
index e2cfb0944dd3..45224eb7a734 100644
--- a/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-c-sharp.json
+++ b/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-c-sharp.json
@@ -1,9 +1,9 @@
 {
   "url": "https://github.com/tree-sitter/tree-sitter-c-sharp",
-  "rev": "5b6ae1f88e741b9ed738891ad1362fb9f2041671",
-  "date": "2022-03-23T15:50:46-04:00",
-  "path": "/nix/store/n5kjbimssqrwz7h99gq83935432dpm5s-tree-sitter-c-sharp",
-  "sha256": "1yp1lyzay7hxlgca2r5yigpdy80vli4f48k2bm3h2rpa99fczmrb",
+  "rev": "fcb2b6f7cb8ab8584d390aa266b0d2df7cbd1fd5",
+  "date": "2022-05-01T16:44:38+01:00",
+  "path": "/nix/store/5kwbva55mi975kqkjrw3jya98cb8i07d-tree-sitter-c-sharp",
+  "sha256": "0xdbh1n1mnglfxn16can69c3sr4ibc37v85vh7ckljcjgqhikfi9",
   "fetchLFS": false,
   "fetchSubmodules": false,
   "deepClone": false,
diff --git a/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-dart.json b/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-dart.json
index 6d79d851fd4d..c222e1faf7d0 100644
--- a/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-dart.json
+++ b/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-dart.json
@@ -1,9 +1,9 @@
 {
   "url": "https://github.com/usernobody14/tree-sitter-dart",
-  "rev": "6a25376685d1d47968c2cef06d4db8d84a70025e",
-  "date": "2021-06-04T09:39:40-06:00",
-  "path": "/nix/store/vdygn1702kn92k222kygk9i50h10z9km-tree-sitter-dart",
-  "sha256": "0z06sphmgjggx5j2rjfy3f85fh1m9s79sql8a7d4kvsamz9rwakl",
+  "rev": "f95876f0ed3ef207bbd3c5c41987bc2e9cecfc97",
+  "date": "2022-05-07T10:16:06-07:00",
+  "path": "/nix/store/aad6q85ni1rp22jkc0n8mhlhjq7pm794-tree-sitter-dart",
+  "sha256": "0iaa37g5z927dvlxla0nidl9n2hvpsw97b5ffi7w1hq9d4m6rc7i",
   "fetchLFS": false,
   "fetchSubmodules": false,
   "deepClone": false,
diff --git a/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-elixir.json b/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-elixir.json
index 2f673c7172ce..abf03571fdbd 100644
--- a/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-elixir.json
+++ b/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-elixir.json
@@ -1,9 +1,9 @@
 {
   "url": "https://github.com/elixir-lang/tree-sitter-elixir",
-  "rev": "ec1c4cac1b2f0290c53511a72fbab17c47815d2b",
-  "date": "2022-04-18T23:16:26+02:00",
-  "path": "/nix/store/2jmkl3lxq6cy0cg4wjf3hgjciw0xsm0y-tree-sitter-elixir",
-  "sha256": "0xiprldyfqpx5fil1b1kbnpj57n7j15j3m8dhibhif7azbd1z1y3",
+  "rev": "5d0c1bfcdf8aaad225525acad930a972b319a675",
+  "date": "2022-04-28T11:17:48-05:00",
+  "path": "/nix/store/a3vks004yjn7pb80nppdyq0k18wm3myc-tree-sitter-elixir",
+  "sha256": "1iff2gk6r6qa13imizxawc4hjwwwsnvhvhafcwab2q2476gk82mz",
   "fetchLFS": false,
   "fetchSubmodules": false,
   "deepClone": false,
diff --git a/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-go.json b/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-go.json
index ca9760bb7e26..53f67d645e7d 100644
--- a/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-go.json
+++ b/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-go.json
@@ -1,9 +1,9 @@
 {
   "url": "https://github.com/tree-sitter/tree-sitter-go",
-  "rev": "c8fed1f0847a65a04a4b8cb7655f5f416e0742ca",
-  "date": "2022-03-29T10:06:48+02:00",
-  "path": "/nix/store/f9vy5q9p3rf2dcp7zdw9708j138ibi36-tree-sitter-go",
-  "sha256": "0yi8h1q39hsdxp9053by9xkl53wn229fhwjrrzml7k8y95qgnsyd",
+  "rev": "372d3241b099e189406475a9445cbb29dac2e054",
+  "date": "2022-04-28T20:49:46+02:00",
+  "path": "/nix/store/ylm4blh7lw1ac3ym9i69gbbs1cc5vmcs-tree-sitter-go",
+  "sha256": "0cmw37lgpfrw82kg9mcx7kgxnnvdydagbwckqv418zbh2xv881jf",
   "fetchLFS": false,
   "fetchSubmodules": false,
   "deepClone": false,
diff --git a/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-haskell.json b/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-haskell.json
index e1d4462e225d..27e64896387e 100644
--- a/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-haskell.json
+++ b/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-haskell.json
@@ -1,9 +1,9 @@
 {
   "url": "https://github.com/tree-sitter/tree-sitter-haskell",
-  "rev": "ed976b81b00ce7b72b99bca75e7a616cc526220c",
-  "date": "2022-03-20T00:05:14+01:00",
-  "path": "/nix/store/wzkfkix4q3vcrlsj2v4q32ihw0vdp1li-tree-sitter-haskell",
-  "sha256": "19g5f59gh6s4xpphrppmrqlh0nfld0q8zffy85pkby4gd6xh73zm",
+  "rev": "ff5c879d9b75f4e6930d7f687d458f707945ad78",
+  "date": "2022-05-07T17:45:16+02:00",
+  "path": "/nix/store/2pnp7kazxg1sp0anf4by99f27d7z0p64-tree-sitter-haskell",
+  "sha256": "0aa960150wli4hnv64jrl4gqvlgchc3y44bx4d7i53ygn9cdkl12",
   "fetchLFS": false,
   "fetchSubmodules": false,
   "deepClone": false,
diff --git a/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-html.json b/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-html.json
index 211e170adced..80034c7cd419 100644
--- a/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-html.json
+++ b/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-html.json
@@ -1,9 +1,9 @@
 {
   "url": "https://github.com/tree-sitter/tree-sitter-html",
-  "rev": "161a92474a7bb2e9e830e48e76426f38299d99d1",
-  "date": "2021-08-17T11:20:56-07:00",
-  "path": "/nix/store/pv8x73j4sbngsqplwfm73jlpwc31mc17-tree-sitter-html",
-  "sha256": "1gwvgwk0py09pp65vnga522l5r16dvgwxsc76fg66y07k2i63cfk",
+  "rev": "29f53d8f4f2335e61bf6418ab8958dac3282077a",
+  "date": "2022-05-06T09:01:49-07:00",
+  "path": "/nix/store/w5dy2r99rbzpmg0icwil5j9cp37l9hkk-tree-sitter-html",
+  "sha256": "0wadphmgndj4vq9mg258624pj0klspbpcx8qlc6f8by5xbshvkmz",
   "fetchLFS": false,
   "fetchSubmodules": false,
   "deepClone": false,
diff --git a/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-java.json b/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-java.json
index 42bd6f10771a..17a9695eed4b 100644
--- a/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-java.json
+++ b/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-java.json
@@ -1,9 +1,9 @@
 {
   "url": "https://github.com/tree-sitter/tree-sitter-java",
-  "rev": "e7cb801ef57f74db5c4ebe14df74de852bb451b5",
-  "date": "2022-04-16T15:36:51+02:00",
-  "path": "/nix/store/55br93464adchwwjwdqjai8ppykwh098-tree-sitter-java",
-  "sha256": "0w27xk9j7mm9gr5aiwcv6cgfvzfnps0l9b09mwfqxhndh7j96vfn",
+  "rev": "39a11c8330d0b2ad75310456c378396785f79a4e",
+  "date": "2022-04-28T20:50:54+02:00",
+  "path": "/nix/store/w2hi6yvm3z4cy3bignphb9c2gf6fpnnq-tree-sitter-java",
+  "sha256": "0im81m2wb35n7rgmraf7p5ql6lvr7m9y4krgmkvgqkxnbkw7zcr0",
   "fetchLFS": false,
   "fetchSubmodules": false,
   "deepClone": false,
diff --git a/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-latex.json b/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-latex.json
index 5b7e511efb19..c06fe54ca044 100644
--- a/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-latex.json
+++ b/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-latex.json
@@ -1,9 +1,9 @@
 {
   "url": "https://github.com/latex-lsp/tree-sitter-latex",
-  "rev": "8c5d90e78fa58ee6acab465ffa9a53e8b7b2c69c",
-  "date": "2022-04-23T15:10:18+02:00",
-  "path": "/nix/store/qpc37mjsl75qnmyzbkw6azphwzfdr9n9-tree-sitter-latex",
-  "sha256": "1xq5g34g9sqshhpprakc4k5lrlgg1n8vb7d7nfrx4ilrz5s0kks1",
+  "rev": "3b370b5ca3948312738b4f27b2a12e4bb58907a2",
+  "date": "2022-05-11T20:22:05+02:00",
+  "path": "/nix/store/l1nja32pv92awd5jnksi3wfd29mqxvkd-tree-sitter-latex",
+  "sha256": "0a4ks4ng02qivxr7h1izhc55791czba2r82ngi7a9l0smdxa9yv7",
   "fetchLFS": false,
   "fetchSubmodules": false,
   "deepClone": false,
diff --git a/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-markdown.json b/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-markdown.json
index a60bf1dffc6b..f33e3022acef 100644
--- a/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-markdown.json
+++ b/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-markdown.json
@@ -1,9 +1,9 @@
 {
   "url": "https://github.com/MDeiml/tree-sitter-markdown",
-  "rev": "d24196f9b3e5af6fcb2ec2a0b6cbc5c06f58b85e",
-  "date": "2022-03-30T11:47:57+02:00",
-  "path": "/nix/store/rdac46kl274bdd18bdrdh33s71sin7xd-tree-sitter-markdown",
-  "sha256": "07i3zwjla74s61w39fqfmb5a61dw6xlgfagh70p1rpvyrpxsywds",
+  "rev": "6d112e7a9c1694504bb78ee0b92dcd509625e0df",
+  "date": "2022-04-26T12:23:01+02:00",
+  "path": "/nix/store/598nrwznzg37r9pskrmzwnhrw3f4knnw-tree-sitter-markdown",
+  "sha256": "03d601dp65p30c88p0r6rx13wlkbg1q3ch11wfn4sa2rhba8zpyk",
   "fetchLFS": false,
   "fetchSubmodules": false,
   "deepClone": false,
diff --git a/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-org-nvim.json b/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-org-nvim.json
index c9b0ce8fcbb3..d29613cc207e 100644
--- a/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-org-nvim.json
+++ b/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-org-nvim.json
@@ -1,9 +1,9 @@
 {
   "url": "https://github.com/milisims/tree-sitter-org",
-  "rev": "fab7af32a2719091df5b222f98099c566859de78",
-  "date": "2022-04-07T16:00:06-04:00",
-  "path": "/nix/store/b17cvbkdvv7d3dzbi58lgrqsnhvh79d8-tree-sitter-org",
-  "sha256": "0jz69wm1ay84zkslbcp4l906ay7l4jd3bi1k1ivclpx493pg8ia7",
+  "rev": "aeacac619457a187bb202b9dfc58541232ed4a25",
+  "date": "2022-05-02T16:54:48-04:00",
+  "path": "/nix/store/y06b3jf6mfgbx4ar9l8crd7r5vljln92-tree-sitter-org",
+  "sha256": "03g52pbnv859wy3sdbr0i440il98idj6zg0q12g7ccxxmwblwxig",
   "fetchLFS": false,
   "fetchSubmodules": false,
   "deepClone": false,
diff --git a/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-php.json b/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-php.json
index c1bc94c210a1..49b6c3c80565 100644
--- a/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-php.json
+++ b/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-php.json
@@ -1,9 +1,9 @@
 {
   "url": "https://github.com/tree-sitter/tree-sitter-php",
-  "rev": "3c17a28da38afac41332d3ce79bbd8951867f346",
-  "date": "2022-03-29T09:09:35-07:00",
-  "path": "/nix/store/7dmygp3gi9ch00mf59d7g2l8k6f2pl81-tree-sitter-php",
-  "sha256": "06xc4y67pl96h1gfh9zg4yxdgqj5mv7md28m78gix8sk1h011irq",
+  "rev": "6be89d517d550a47b067b23d0f89a364091b41ca",
+  "date": "2022-05-04T13:05:38-04:00",
+  "path": "/nix/store/pd19zya0sng7dahwgkamk51s1mprg9hf-tree-sitter-php",
+  "sha256": "18yrmvxajcg7m8xqpdkdllm9grs4m9pp4y058ky6q3drq7cx0v1m",
   "fetchLFS": false,
   "fetchSubmodules": false,
   "deepClone": false,
diff --git a/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-pug.json b/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-pug.json
index cf72f03519cd..6e27d64bec74 100644
--- a/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-pug.json
+++ b/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-pug.json
@@ -1,9 +1,9 @@
 {
   "url": "https://github.com/zealot128/tree-sitter-pug",
-  "rev": "5875f9a7d94836708119b0a1102bb5792e8bf673",
-  "date": "2021-07-13T22:48:45+02:00",
-  "path": "/nix/store/3bwj01nmxkd4cmvjyrfv2a6wq07hbqig-tree-sitter-pug",
-  "sha256": "1sjw632yidi8dq34g1nqmld9861j40qnrlg4c8w478kl8hmhnvmb",
+  "rev": "63e214905970e75f065688b1e8aa90823c3aacdc",
+  "date": "2022-05-05T14:29:30+02:00",
+  "path": "/nix/store/8nwqja3ff6cmy06sgxx6wzlbg7qx6x1r-tree-sitter-pug",
+  "sha256": "1r3zhz4adfpg2ihlbdfx4nb9svv6apnlahgfqqzmacj3bm8r3wmp",
   "fetchLFS": false,
   "fetchSubmodules": false,
   "deepClone": false,
diff --git a/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-ql.json b/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-ql.json
index d1a73a02c0b4..66359662e7c6 100644
--- a/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-ql.json
+++ b/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-ql.json
@@ -1,9 +1,9 @@
 {
   "url": "https://github.com/tree-sitter/tree-sitter-ql",
-  "rev": "8e7fd7e638d4a0ec7a792ee16b19dbc6407aa810",
-  "date": "2021-06-02T18:46:47+02:00",
-  "path": "/nix/store/yhyi9y09shv1fm87gka43vnv9clvyd92-tree-sitter-ql",
-  "sha256": "0x5f9989ymqvw3g8acckyk4j7zpmnc667qishbgly9icl9rkmv7w",
+  "rev": "b2c2364e833cc9f1afa243ac367f1475330fef63",
+  "date": "2022-05-04T13:16:04-04:00",
+  "path": "/nix/store/8c01j930llm5wacj2727k8igwwyhbcz4-tree-sitter-ql",
+  "sha256": "1a4k4rmyqqcj94y57sf2h27bbkn921p1ifl2xwcqpmk6dr6n5bbr",
   "fetchLFS": false,
   "fetchSubmodules": false,
   "deepClone": false,
diff --git a/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-rust.json b/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-rust.json
index 670103d5c78d..36508dc4769c 100644
--- a/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-rust.json
+++ b/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-rust.json
@@ -1,9 +1,9 @@
 {
   "url": "https://github.com/tree-sitter/tree-sitter-rust",
-  "rev": "0509e440ae042db6483984b3a56b3c5f24b5d9b9",
-  "date": "2022-03-09T12:11:47+01:00",
-  "path": "/nix/store/9jrsqsrql5wlbzmqna111w4a02hf75z2-tree-sitter-rust",
-  "sha256": "1r8n8441b8bppizlzh4xw7yy3amz4apfxpqxm8hw0n3j3iwnw4pz",
+  "rev": "9a6d980afbb9864405426f1b3905fbcd459871ca",
+  "date": "2022-05-09T16:14:09-07:00",
+  "path": "/nix/store/h5zks31j4xj7vw5ygqhbml0ydsly7l6z-tree-sitter-rust",
+  "sha256": "0hmamkb2hqrp67b756ckifbwdbr0yw7qr2m8farh0bg7rbi5c6z1",
   "fetchLFS": false,
   "fetchSubmodules": false,
   "deepClone": false,
diff --git a/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-scala.json b/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-scala.json
index bf15e656e914..4cdaa55dd286 100644
--- a/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-scala.json
+++ b/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-scala.json
@@ -1,9 +1,9 @@
 {
   "url": "https://github.com/tree-sitter/tree-sitter-scala",
-  "rev": "ec6047f531e7d4c13787d4ff208b94a84de34165",
-  "date": "2022-03-27T09:48:17+02:00",
-  "path": "/nix/store/70sghy226gl3s1b2p0zjhplb6zjy777g-tree-sitter-scala",
-  "sha256": "0yjl8hwdm1pkihfgfbg19z5j0v3cp64a2pa59maws1i231fm5bsw",
+  "rev": "8599058ef292e82203a1b23d10734dcbaf4d1b5c",
+  "date": "2022-05-09T16:17:13-07:00",
+  "path": "/nix/store/q802q124fq79wwr6m4xfcdmgw6fzjigw-tree-sitter-scala",
+  "sha256": "0i6qkgyv722jwma2rs0nf02jzl5dvml5m1whb7580qnza95x7py1",
   "fetchLFS": false,
   "fetchSubmodules": false,
   "deepClone": false,
diff --git a/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-vim.json b/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-vim.json
index b9a3184e942e..10908da4ae7c 100644
--- a/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-vim.json
+++ b/pkgs/development/tools/parsing/tree-sitter/grammars/tree-sitter-vim.json
@@ -1,9 +1,9 @@
 {
   "url": "https://github.com/vigoux/tree-sitter-viml",
-  "rev": "5268e0ec901e33ad7142ee31b580269a94fba042",
-  "date": "2022-04-16T20:12:40+02:00",
-  "path": "/nix/store/rw6cjm4vj4yihlfmrxa2vc81lr3x59rn-tree-sitter-viml",
-  "sha256": "0vga1bivzkr00brzvv309hx7sqvg7y2kf6vx0s8hv9r56x6nm54s",
+  "rev": "4b9d2dda6de64fe5abc9bf96b5727ba73ed08515",
+  "date": "2022-05-07T11:41:23+02:00",
+  "path": "/nix/store/zm2pfjv3fn2qg6iy1s03mn5kjawsy3qg-tree-sitter-viml",
+  "sha256": "0p7fj5vvxxz4d43j91zwv3h8df4m4c26w9gq2qx561vjh5w1q7fn",
   "fetchLFS": false,
   "fetchSubmodules": false,
   "deepClone": false,
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index 9c3e666c5b3b..6cfd34aa279b 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -1,4 +1,5 @@
-{ lib, stdenv, callPackage, newScope, recurseIntoAttrs, ocamlPackages_4_05, ocamlPackages_4_09
+{ lib, stdenv, fetchzip
+, callPackage, newScope, recurseIntoAttrs, ocamlPackages_4_05, ocamlPackages_4_09
 , ocamlPackages_4_10, ocamlPackages_4_12, fetchpatch, makeWrapper, coq2html
 }@args:
 let lib = import ../build-support/coq/extra-lib.nix {inherit (args) lib;}; in
@@ -8,6 +9,8 @@ let
       inherit coq lib;
       coqPackages = self;
 
+      metaFetch = import ../build-support/coq/meta-fetch/default.nix
+        {inherit lib stdenv fetchzip; };
       mkCoqDerivation = callPackage ../build-support/coq {};
 
       contribs = recurseIntoAttrs