coqPackages: etc

- put `findlib` in `buildInputs` of `mkCoqDerivation` to make sure `coq` packages find their ocaml plugin dependencies,
- use `propagatedBuildInputs` to make sure ocaml plugin dependencies are in path,
- updated `coqPackage.heq` (broken url),
- fixed use of `DESTDIR` and `COQMF_COQLIB` in mkCoqDerivation,
- adding `COQCORELIB` environement variable to put ocaml plugin files in the right place,
- make `metaFetch` available from `coqPackages`

30 files changed, 78 insertions, 91 deletions

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..847ef8af23fe 100644
--- a/pkgs/development/coq-modules/compcert/default.nix
+++ b/pkgs/development/coq-modules/compcert/default.nix
@@ -1,4 +1,5 @@
-{ lib, fetchzip, mkCoqDerivation, coq, flocq, compcert
+{ lib, fetchzip, mkCoqDerivation
+, coq, flocq, compcert
 , ocamlPackages, fetchpatch, makeWrapper, coq2html
 , stdenv, tools ? stdenv.cc
 , version ? null
@@ -15,9 +16,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 = {
@@ -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=";
-    };
-  };
-
-  extraBuildInputs = [ mathcomp.ssreflect mathcomp.fingroup ];
-  propagatedBuildInputs = [ mathcomp.algebra ];
+  release."1.1.0".sha256 = "sha256-TCw1kSXeW0ysIdLeNr+EGmpGumEE9i8tinEMp57UXaE=";
+  release."1.0.0".sha256 = "0nv5mdgrd075dpd8bc7h0xc5i95v0pkm0bfyq5rj6ii1s54dwcjl";
 
-  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 375fae5b074c..1a47478bda15 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..40d1c3d9b31c 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