diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix
new file mode 100644
index 00000000000..475c68f7b9c
--- /dev/null
+++ b/pkgs/applications/science/logic/coq/default.nix
@@ -0,0 +1,23 @@
+{stdenv, fetchurl, ocaml, ncurses}:
+
+stdenv.mkDerivation (rec {
+
+  name = "coq-8.1pl3";
+  src = fetchurl {
+    url = "http://coq.inria.fr/V8.1pl3/files/coq-8.1pl3.tar.gz";
+    sha256 = "7f8f45594adff2625312c5ecb144cb00d39c99201dac309c9286b34d01a36bb6";
+  };
+
+  buildInputs = [ocaml ncurses];
+
+  prefixKey = "-prefix ";
+  patchPhase = ''
+    UNAME=$(type -tp uname)
+    MV=$(type -tp mv)
+    RM=$(type -tp cp)
+    substituteInPlace ./configure --replace "/bin/uname" "$UNAME"
+    substituteInPlace Makefile --replace "/bin/mv" "$MV" \
+                               --replace "/bin/rm" "$RM"
+  '';
+
+})
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 35583bf59e5..3d31a126f25 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -6789,6 +6789,11 @@ let pkgs = rec {
     inherit fetchurl stdenv;
   };
 
+  ### SCIENCE/LOGIC
+
+  coq = import ../applications/science/logic/coq {
+    inherit fetchurl stdenv ocaml ncurses;
+  };
 
   ### MISC