diff --git a/pkgs/applications/science/logic/coq/8.5.nix b/pkgs/applications/science/logic/coq/8.5.nix
index eb74891f511c..aae2101f50e9 100644
--- a/pkgs/applications/science/logic/coq/8.5.nix
+++ b/pkgs/applications/science/logic/coq/8.5.nix
@@ -2,11 +2,22 @@
 # - The csdp program used for the Micromega tactic is statically referenced.
 #   However, coq can build without csdp by setting it to null.
 #   In this case some Micromega tactics will search the user's path for the csdp program and will fail if it is not found.
+# - The patch-level version can be specified through the `pl` argument to
+#   the derivation; it defaults to the greatest.
 
-{stdenv, fetchurl, writeText, pkgconfig, ocaml, findlib, camlp5, ncurses, lablgtk ? null, csdp ? null}:
+{ stdenv, fetchurl, writeText, pkgconfig
+, ocaml, findlib, camlp5, ncurses
+, lablgtk ? null, csdp ? null
+, pl ? "3"
+}:
 
 let
-  version = "8.5pl2";
+  version = "8.5pl${pl}";
+  sha256 = {
+   "1" = "1w2xvm6w16khfn63bp95s25hnkn2ny3w0yqg3lq63gp11aqpbyjb";
+   "2" = "0wyywia0darak2zmc5v0ra9rn0b9whwdfiahralm8v5za499s8w3";
+   "3" = "0fyk2a4fpifibq8y8jhx1891k55qnsnlygglch64sva0bph94nrh";
+  }."${pl}";
   coq-version = "8.5";
   buildIde = lablgtk != null;
   ideFlags = if buildIde then "-lablgtkdir ${lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt" else "";
@@ -24,7 +35,7 @@ stdenv.mkDerivation {
 
   src = fetchurl {
     url = "http://coq.inria.fr/distrib/V${version}/files/coq-${version}.tar.gz";
-    sha256 = "0wyywia0darak2zmc5v0ra9rn0b9whwdfiahralm8v5za499s8w3";
+    inherit sha256;
   };
 
   buildInputs = [ pkgconfig ocaml findlib camlp5 ncurses lablgtk ];
@@ -34,7 +45,7 @@ stdenv.mkDerivation {
     RM=$(type -tp rm)
     substituteInPlace configure --replace "/bin/uname" "$UNAME"
     substituteInPlace tools/beautify-archive --replace "/bin/rm" "$RM"
-    substituteInPlace configure.ml --replace "if arch = \"Darwin\" || arch = \"FreeBSD\" then \"md5" "if arch = \"Darwinx\" then \"md5"
+    substituteInPlace configure.ml --replace '"md5 -q"' '"md5sum"'
     ${csdpPatch}
   '';
 
@@ -57,7 +68,11 @@ stdenv.mkDerivation {
 
   prefixKey = "-prefix ";
 
-  buildFlags = "revision coq coqide";
+  buildFlags = "revision coq coqide bin/votour";
+
+  postInstall = ''
+    cp bin/votour $out/bin/
+  '';
 
   meta = with stdenv.lib; {
     description = "Coq proof assistant";
diff --git a/pkgs/development/compilers/compcert/default.nix b/pkgs/development/compilers/compcert/default.nix
index fb95372a96f7..f5554ee0ce39 100644
--- a/pkgs/development/compilers/compcert/default.nix
+++ b/pkgs/development/compilers/compcert/default.nix
@@ -19,6 +19,7 @@ stdenv.mkDerivation rec {
   enableParallelBuilding = true;
 
   configurePhase = ''
+    substituteInPlace ./configure --replace pl2 pl3
     substituteInPlace ./configure --replace '{toolprefix}gcc' '{toolprefix}cc'
     ./configure -prefix $out -toolprefix ${tools}/bin/ '' +
     (if stdenv.isDarwin then "ia32-macosx" else "ia32-linux");
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index f95f0415fd98..d8ab2993447e 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -16487,13 +16487,27 @@ in
 
   aspino = callPackage ../applications/science/logic/aspino {};
 
-  inherit (ocaml-ng.ocamlPackages_4_01_0) coq;
+  coq = callPackage ../applications/science/logic/coq {
+    inherit (ocamlPackages_4_01_0) ocaml findlib lablgtk;
+    camlp5 = ocamlPackages_4_01_0.camlp5_transitional;
+  };
 
-  inherit (ocamlPackages) coq_HEAD;
+  coq_HEAD = callPackage ../applications/science/logic/coq/HEAD.nix {
+    inherit (ocamlPackages) ocaml findlib lablgtk;
+    camlp5 = ocamlPackages.camlp5_transitional;
+  };
 
-  inherit (ocamlPackages) coq_8_5;
+  coq_8_5 = callPackage ../applications/science/logic/coq/8.5.nix {
+    inherit (ocamlPackages) ocaml findlib lablgtk;
+    camlp5 = ocamlPackages.camlp5_transitional;
+  };
 
-  inherit (ocaml-ng.ocamlPackages_3_12_1) coq_8_3;
+  coq_8_3 = callPackage ../applications/science/logic/coq/8.3.nix {
+    make = pkgs.gnumake3;
+    inherit (ocamlPackages_3_12_1) ocaml findlib;
+    camlp5 = ocamlPackages_3_12_1.camlp5_transitional;
+    lablgtk = ocamlPackages_3_12_1.lablgtk_2_14;
+  };
 
   mkCoqPackages_8_4 = self: let callPackage = newScope self; in {
 
diff --git a/pkgs/top-level/ocaml-packages.nix b/pkgs/top-level/ocaml-packages.nix
index 873ce337a09f..2c83fe81737e 100644
--- a/pkgs/top-level/ocaml-packages.nix
+++ b/pkgs/top-level/ocaml-packages.nix
@@ -630,7 +630,7 @@ let
       then { tools = pkgs.pkgsi686Linux.stdenv.cc; }
       else {}
     ) // {
-      coq = coq_8_5;
+      coq = pkgs.coq_8_5;
     });
 
     haxe = callPackage ../development/compilers/haxe { };
@@ -672,24 +672,6 @@ let
       enableX11 = config.unison.enableX11 or true;
     };
 
-    coq = callPackage ../applications/science/logic/coq {
-      camlp5 = camlp5_transitional;
-    };
-
-    coq_HEAD = callPackage ../applications/science/logic/coq/HEAD.nix {
-      camlp5 = camlp5_transitional;
-    };
-
-    coq_8_5 = callPackage ../applications/science/logic/coq/8.5.nix {
-      camlp5 = camlp5_transitional;
-    };
-
-    coq_8_3 = callPackage ../applications/science/logic/coq/8.3.nix {
-      make = pkgs.gnumake3;
-      camlp5 = camlp5_transitional;
-      lablgtk = lablgtk_2_14;
-    };
-
     hol_light = callPackage ../applications/science/logic/hol_light {
       camlp5 = camlp5_strict;
     };