diff --git a/pkgs/applications/science/logic/coq/configure.patch.gz b/pkgs/applications/science/logic/coq/configure.patch.gz
new file mode 100644
index 000000000000..85ecfda6dae1
Binary files /dev/null and b/pkgs/applications/science/logic/coq/configure.patch.gz differ
diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix
index 475c68f7b9cf..19827022072d 100644
--- a/pkgs/applications/science/logic/coq/default.nix
+++ b/pkgs/applications/science/logic/coq/default.nix
@@ -1,23 +1,66 @@
-{stdenv, fetchurl, ocaml, ncurses}:
+# TODO:
+# - coqide compilation should be optional or (better) separate;
+# - coqide libraries are not installed;
 
-stdenv.mkDerivation (rec {
+{stdenv, fetchurl, ocaml, camlp5, lablgtk, ncurses}:
+
+let
+
+  pname = "coq";
+  version = "8.2pl1";
+  name = "${pname}-${version}";
+
+in
+
+stdenv.mkDerivation {
+  inherit name;
 
-  name = "coq-8.1pl3";
   src = fetchurl {
-    url = "http://coq.inria.fr/V8.1pl3/files/coq-8.1pl3.tar.gz";
-    sha256 = "7f8f45594adff2625312c5ecb144cb00d39c99201dac309c9286b34d01a36bb6";
+    url = "http://coq.inria.fr/V${version}/files/${name}.tar.gz";
+    sha256 = "7c15acfd369111e51d937cce632d22fc77a6718a5ac9f2dd2dcbdfab4256ae0c";
   };
 
-  buildInputs = [ocaml ncurses];
+  buildInputs = [ ocaml camlp5 ncurses lablgtk ];
 
   prefixKey = "-prefix ";
-  patchPhase = ''
+
+  configureFlags =
+    "-camldir ${ocaml}/bin " +
+    "-camlp5dir ${camlp5}/lib/ocaml/camlp5 " +
+    "-lablgtkdir ${lablgtk}/lib/ocaml/lablgtk2 " +
+    "-opt -coqide opt";
+
+  buildFlags = "world"; # Debug with "world VERBOSE=1";
+
+  patches = [ ./configure.patch.gz ];
+
+  postPatch = ''
+    BASH=$(type -tp bash)
     UNAME=$(type -tp uname)
     MV=$(type -tp mv)
-    RM=$(type -tp cp)
-    substituteInPlace ./configure --replace "/bin/uname" "$UNAME"
-    substituteInPlace Makefile --replace "/bin/mv" "$MV" \
+    RM=$(type -tp rm)
+    substituteInPlace configure --replace "/bin/bash" "$BASH" \
+                                --replace "/bin/uname" "$UNAME"
+    substituteInPlace Makefile --replace "/bin/bash" "$BASH" \
+                               --replace "/bin/mv" "$MV" \
                                --replace "/bin/rm" "$RM"
+    substituteInPlace Makefile.stage1 --replace "/bin/bash" "$BASH"
+    substituteInPlace install.sh --replace "/bin/bash" "$BASH"
+    substituteInPlace dev/v8-syntax/check-grammar --replace "/bin/bash" "$BASH"
+    substituteInPlace scripts/coqmktop.ml --replace \
+      "\"-I\"; \"+lablgtk2\"" \
+      "\"-I\"; \"${lablgtk}/lib/ocaml/lablgtk2\"; \"-I\"; \"${lablgtk}/lib/ocaml/stublibs\""
   '';
 
-})
+  meta = {
+    description = "Coq proof assistant";
+    longDescription = ''
+      Coq is a formal proof management system.  It provides a formal language
+      to write mathematical definitions, executable algorithms and theorems
+      together with an environment for semi-interactive development of
+      machine-checked proofs.
+    '';
+    homepage = "http://coq.inria.fr";
+    license = "LGPL";
+  };
+}
diff --git a/pkgs/development/tools/ocaml/camlp5/default.nix b/pkgs/development/tools/ocaml/camlp5/default.nix
index b630c05fe53f..7c87243054bd 100644
--- a/pkgs/development/tools/ocaml/camlp5/default.nix
+++ b/pkgs/development/tools/ocaml/camlp5/default.nix
@@ -24,7 +24,7 @@ stdenv.mkDerivation {
   buildFlags = "world.opt";
 
   meta = {
-    description = "Preprocessor-pretty-printer for OCaml.";
+    description = "Preprocessor-pretty-printer for OCaml";
     longDescription = ''
       Camlp5 is a preprocessor and pretty-printer for OCaml programs.
       It also provides parsing and printing tools.
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 15c73649583b..af6ea52bee60 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -2662,6 +2662,15 @@ let
     inherit fetchurl stdenv;
   };
 
+  camlp5_strict = import ../development/tools/ocaml/camlp5 {
+    inherit stdenv fetchurl ocaml;
+  };
+
+  camlp5_transitional = import ../development/tools/ocaml/camlp5 {
+    inherit stdenv fetchurl ocaml;
+    transitional = true;
+  };
+
   ccache = import ../development/tools/misc/ccache {
     inherit fetchurl stdenv;
   };
@@ -5220,13 +5229,6 @@ let
     inherit libuuid zlib acl;
   };
 
-  camlp5_strict = import ../development/tools/ocaml/camlp5
-    { inherit stdenv fetchurl ocaml; };
-
-  camlp5_transitional = import ../development/tools/ocaml/camlp5
-    { inherit stdenv fetchurl ocaml;
-      transitional = true; };
-
   cpufrequtils = (
     import ../os-specific/linux/cpufrequtils {
     inherit fetchurl stdenv libtool gettext;
@@ -8278,10 +8280,10 @@ let
   ### SCIENCE/LOGIC
 
   coq = import ../applications/science/logic/coq {
-    inherit fetchurl stdenv ocaml ncurses;
+    inherit stdenv fetchurl ocaml lablgtk ncurses;
+    camlp5 = camlp5_transitional;
   };
 
-
   ### SCIENCE / ELECTRONICS
 
   ngspice = import ../applications/science/electronics/ngspice {