diff --git a/doc/languages-frameworks/coq.xml b/doc/languages-frameworks/coq.xml
index d5f2574039f2..640b04c7da9d 100644
--- a/doc/languages-frameworks/coq.xml
+++ b/doc/languages-frameworks/coq.xml
@@ -11,10 +11,9 @@
  </para>
 
  <para>
-  Some libraries require OCaml and sometimes also Camlp5 or findlib. The exact
-  versions that were used to build Coq are saved in the
-  <literal>coq.ocaml</literal> and <literal>coq.camlp5</literal> and
-  <literal>coq.findlib</literal> attributes.
+  Some extensions (plugins) might require OCaml and sometimes other OCaml
+  packages. The <literal>coq.ocamlPackages</literal> attribute can be used
+  to depend on the same package set Coq was built against.
  </para>
 
  <para>
diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix
index 23f1ff85edf0..040d722f9410 100644
--- a/pkgs/applications/science/logic/coq/default.nix
+++ b/pkgs/applications/science/logic/coq/default.nix
@@ -37,6 +37,8 @@ self = stdenv.mkDerivation {
 
   passthru = {
     inherit coq-version;
+    inherit ocamlPackages;
+    # For compatibility
     inherit (ocamlPackages) ocaml camlp5 findlib num;
     emacsBufferSetup = pkgs: ''
       ; Propagate coq paths to children
diff --git a/pkgs/development/coq-modules/QuickChick/default.nix b/pkgs/development/coq-modules/QuickChick/default.nix
index fc88a1c33eed..d532020d663c 100644
--- a/pkgs/development/coq-modules/QuickChick/default.nix
+++ b/pkgs/development/coq-modules/QuickChick/default.nix
@@ -33,7 +33,7 @@ stdenv.mkDerivation rec {
     inherit (param) rev sha256;
   };
 
-  buildInputs = [ coq.ocaml coq.camlp5 coq.findlib ];
+  buildInputs = with coq.ocamlPackages; [ ocaml camlp5 findlib ];
   propagatedBuildInputs = [ coq ssreflect ];
 
   enableParallelBuilding = false;
diff --git a/pkgs/development/coq-modules/bignums/default.nix b/pkgs/development/coq-modules/bignums/default.nix
index 474ce05c1d47..e645a3424c0d 100644
--- a/pkgs/development/coq-modules/bignums/default.nix
+++ b/pkgs/development/coq-modules/bignums/default.nix
@@ -28,7 +28,7 @@ stdenv.mkDerivation rec {
     inherit (param) rev sha256;
   };
 
-  buildInputs = [ coq.ocaml coq.camlp5 coq.findlib coq ];
+  buildInputs = with coq.ocamlPackages; [ ocaml camlp5 findlib coq ];
 
   installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
 
diff --git a/pkgs/development/coq-modules/category-theory/default.nix b/pkgs/development/coq-modules/category-theory/default.nix
index c707fcdbd6be..4587e08be483 100644
--- a/pkgs/development/coq-modules/category-theory/default.nix
+++ b/pkgs/development/coq-modules/category-theory/default.nix
@@ -26,7 +26,7 @@ stdenv.mkDerivation rec {
     inherit (param) rev sha256;
   };
 
-  buildInputs = [ coq.ocaml coq.camlp5 coq.findlib ];
+  buildInputs = with coq.ocamlPackages; [ ocaml camlp5 findlib ];
   propagatedBuildInputs = [ coq ssreflect ];
 
   enableParallelBuilding = false;
diff --git a/pkgs/development/coq-modules/contribs/default.nix b/pkgs/development/coq-modules/contribs/default.nix
index 1b310d74b82a..d12d3fefb944 100644
--- a/pkgs/development/coq-modules/contribs/default.nix
+++ b/pkgs/development/coq-modules/contribs/default.nix
@@ -12,7 +12,7 @@ let mkContrib = repo: revs: param:
       sha256 = "${param.sha256}";
     };
 
-    buildInputs = [ coq.ocaml coq.camlp5 coq.findlib coq ];
+    buildInputs = with coq.ocamlPackages; [ ocaml camlp5 findlib coq ];
 
     installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/";
 
diff --git a/pkgs/development/coq-modules/coq-ext-lib/default.nix b/pkgs/development/coq-modules/coq-ext-lib/default.nix
index 5e6ee7fac6f1..0e9c0b93ceda 100644
--- a/pkgs/development/coq-modules/coq-ext-lib/default.nix
+++ b/pkgs/development/coq-modules/coq-ext-lib/default.nix
@@ -22,7 +22,7 @@ stdenv.mkDerivation rec {
     inherit (param) sha256;
   };
 
-  buildInputs = [ coq.ocaml coq.camlp5 ];
+  buildInputs = with coq.ocamlPackages; [ ocaml camlp5 ];
   propagatedBuildInputs = [ coq ];
 
   enableParallelBuilding = true;
diff --git a/pkgs/development/coq-modules/coq-haskell/default.nix b/pkgs/development/coq-modules/coq-haskell/default.nix
index cbfd79fdd272..57f31e1847c1 100644
--- a/pkgs/development/coq-modules/coq-haskell/default.nix
+++ b/pkgs/development/coq-modules/coq-haskell/default.nix
@@ -38,7 +38,7 @@ stdenv.mkDerivation rec {
     inherit (param) rev sha256;
   };
 
-  buildInputs = [ coq.ocaml coq.camlp5 coq.findlib ];
+  buildInputs = with coq.ocamlPackages; [ ocaml camlp5 findlib ];
   propagatedBuildInputs = [ coq ssreflect ];
 
   enableParallelBuilding = false;
diff --git a/pkgs/development/coq-modules/dpdgraph/default.nix b/pkgs/development/coq-modules/dpdgraph/default.nix
index 5b9437e7c279..e403f7d4fb5c 100644
--- a/pkgs/development/coq-modules/dpdgraph/default.nix
+++ b/pkgs/development/coq-modules/dpdgraph/default.nix
@@ -1,4 +1,4 @@
-{ stdenv, fetchFromGitHub, autoreconfHook, coq, ocamlPackages }:
+{ stdenv, fetchFromGitHub, autoreconfHook, coq }:
 
 let params = {
   "8.8" = {
@@ -34,8 +34,8 @@ stdenv.mkDerivation {
   };
 
   nativeBuildInputs = [ autoreconfHook ];
-  buildInputs = [ coq coq.camlp5 ]
-  ++ (with ocamlPackages; [ ocaml findlib ocamlgraph ]);
+  buildInputs = [ coq ]
+  ++ (with coq.ocamlPackages; [ ocaml camlp5 findlib ocamlgraph ]);
 
   preInstall = ''
     mkdir -p $out/bin
diff --git a/pkgs/development/coq-modules/equations/default.nix b/pkgs/development/coq-modules/equations/default.nix
index fa17d37b4bd3..3f049eed34be 100644
--- a/pkgs/development/coq-modules/equations/default.nix
+++ b/pkgs/development/coq-modules/equations/default.nix
@@ -35,7 +35,7 @@ stdenv.mkDerivation rec {
     sha256 = "${param.sha256}";
   };
 
-  buildInputs = [ coq.ocaml coq.camlp5 coq.findlib coq ];
+  buildInputs = with coq.ocamlPackages; [ ocaml camlp5 findlib coq ];
 
   preBuild = "coq_makefile -f _CoqProject -o Makefile";
 
diff --git a/pkgs/development/coq-modules/fiat/HEAD.nix b/pkgs/development/coq-modules/fiat/HEAD.nix
index b970747c7726..a064064fd919 100644
--- a/pkgs/development/coq-modules/fiat/HEAD.nix
+++ b/pkgs/development/coq-modules/fiat/HEAD.nix
@@ -11,7 +11,7 @@ stdenv.mkDerivation rec {
     sha256 = "0griqc675yylf9rvadlfsabz41qy5f5idya30p5rv6ysiakxya64";
   };
 
-  buildInputs = [ coq.ocaml coq.camlp5 python27 ];
+  buildInputs = with coq.ocamlPackages; [ ocaml camlp5 python27 ];
   propagatedBuildInputs = [ coq ];
 
   doCheck = false;
diff --git a/pkgs/development/coq-modules/flocq/default.nix b/pkgs/development/coq-modules/flocq/default.nix
index 092337125a4d..ff7385a9222e 100644
--- a/pkgs/development/coq-modules/flocq/default.nix
+++ b/pkgs/development/coq-modules/flocq/default.nix
@@ -10,7 +10,7 @@ stdenv.mkDerivation rec {
     sha256 = "13fv150dcwnjrk00d7zj2c5x9jwmxgrq0ay440gkr730l8mvk3l3";
   };
 
-  buildInputs = [ coq.ocaml coq.camlp5 bash which autoconf automake ];
+  buildInputs = with coq.ocamlPackages; [ ocaml camlp5 bash which autoconf automake ];
   propagatedBuildInputs = [ coq ];
 
   buildPhase = ''
diff --git a/pkgs/development/coq-modules/heq/default.nix b/pkgs/development/coq-modules/heq/default.nix
index bf441562b14e..03149bab58b1 100644
--- a/pkgs/development/coq-modules/heq/default.nix
+++ b/pkgs/development/coq-modules/heq/default.nix
@@ -10,7 +10,7 @@ stdenv.mkDerivation rec {
     sha256 = "03y71c4qs6cmy3s2hjs05g7pcgk9sqma6flj15394yyxbvr9is1p";
   };
 
-  buildInputs = [ coq.ocaml coq.camlp5 unzip ];
+  buildInputs = with coq.ocamlPackages; [ ocaml camlp5 unzip ];
   propagatedBuildInputs = [ coq ];
 
   preBuild = "cd src";
diff --git a/pkgs/development/coq-modules/mathcomp/generic.nix b/pkgs/development/coq-modules/mathcomp/generic.nix
index 22721ca98bc2..2a602711965f 100644
--- a/pkgs/development/coq-modules/mathcomp/generic.nix
+++ b/pkgs/development/coq-modules/mathcomp/generic.nix
@@ -9,7 +9,7 @@ stdenv.mkDerivation {
   inherit src;
 
   nativeBuildInputs = stdenv.lib.optionals withDoc [ graphviz ];
-  buildInputs = [ coq.ocaml coq.findlib coq.camlp5 ncurses which ];
+  buildInputs = with coq.ocamlPackages; [ ocaml findlib camlp5 ncurses which ];
   propagatedBuildInputs = [ coq ];
 
   enableParallelBuilding = true;
diff --git a/pkgs/development/coq-modules/metalib/default.nix b/pkgs/development/coq-modules/metalib/default.nix
index f6316f77a1fa..46a6cafb6ab8 100644
--- a/pkgs/development/coq-modules/metalib/default.nix
+++ b/pkgs/development/coq-modules/metalib/default.nix
@@ -29,7 +29,7 @@ stdenv.mkDerivation rec {
     license = stdenv.lib.licenses.mit;
   };
 
-  buildInputs = [ coq.ocaml coq.camlp5 which coq lngen ott coq.findlib ];
+  buildInputs = with coq.ocamlPackages; [ ocaml camlp5 which coq lngen ott findlib ];
   propagatedBuildInputs = [ coq ];
 
   enableParallelBuilding = true;
diff --git a/pkgs/development/coq-modules/paco/default.nix b/pkgs/development/coq-modules/paco/default.nix
index 94a24eb70858..86a1301d3c76 100644
--- a/pkgs/development/coq-modules/paco/default.nix
+++ b/pkgs/development/coq-modules/paco/default.nix
@@ -10,7 +10,7 @@ stdenv.mkDerivation rec {
     sha256 = "1lcmdr0y2d7gzyvr8dal3pi7fibbd60bpi1l32fw89xiyrgqhsqy";
   };
 
-  buildInputs = [ coq.ocaml coq.camlp5 unzip ];
+  buildInputs = with coq.ocamlPackages; [ ocaml camlp5 unzip ];
   propagatedBuildInputs = [ coq ];
 
   preBuild = "cd src";
diff --git a/pkgs/development/coq-modules/ssreflect/generic.nix b/pkgs/development/coq-modules/ssreflect/generic.nix
index d09e47a7f845..23e364cd960d 100644
--- a/pkgs/development/coq-modules/ssreflect/generic.nix
+++ b/pkgs/development/coq-modules/ssreflect/generic.nix
@@ -9,7 +9,7 @@ stdenv.mkDerivation {
   inherit src;
 
   nativeBuildInputs = stdenv.lib.optionals withDoc [ graphviz ];
-  buildInputs = [ coq.ocaml coq.findlib coq.camlp5 ncurses which ];
+  buildInputs = with coq.ocamlPackages; [ ocaml findlib camlp5 ncurses which ];
   propagatedBuildInputs = [ coq ];
 
   enableParallelBuilding = true;