diff --git a/pkgs/applications/science/logic/coq/beta.nix b/pkgs/applications/science/logic/coq/beta.nix
new file mode 100644
index 000000000000..c5c4221ac1ee
--- /dev/null
+++ b/pkgs/applications/science/logic/coq/beta.nix
@@ -0,0 +1,53 @@
+# TODO:
+# - coqide compilation should be optional or (better) separate;
+# - coqide libraries are not installed;
+
+{stdenv, fetchurl, ocaml, camlp5, lablgtk, ncurses}:
+
+stdenv.mkDerivation {
+  name = "coq-8.3-beta0-1";
+
+  src = fetchurl {
+    url = http://coq.inria.fr/distrib/V8.3-beta0/files/coq-8.3-beta0-1.tar.gz;
+    sha256 = "01m1x0gpzfsiybyqanm82ls8q63q0g2d9vvfs99zf4z1nny7vlf1";
+  };
+
+  buildInputs = [ ocaml camlp5 ncurses lablgtk ];
+
+  prefixKey = "-prefix ";
+
+  preConfigure = ''
+    ARCH=`uname -s`
+    CAMLDIR=`type -p ocamlc`
+  '';
+
+  configureFlags =
+    "-arch $ARCH " +
+    "-camldir $CAMLDIR " +
+    "-camldir ${ocaml}/bin " +
+    "-camlp5dir ${camlp5}/lib/ocaml/camlp5 " +
+    "-lablgtkdir ${lablgtk}/lib/ocaml/lablgtk2 " +
+    "-opt -coqide opt";
+
+  buildFlags = "world"; # Debug with "world VERBOSE=1";
+
+  patches = [ ./coq-8.3-beta0-1.patch ];
+
+  postPatch = ''
+    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/applications/science/logic/coq/coq-8.3-beta0-1.patch b/pkgs/applications/science/logic/coq/coq-8.3-beta0-1.patch
new file mode 100644
index 000000000000..a5259eb43c08
--- /dev/null
+++ b/pkgs/applications/science/logic/coq/coq-8.3-beta0-1.patch
@@ -0,0 +1,20 @@
+diff -Nurp coq-8.3-beta0-1/configure coq-8.3-beta0-1-nix/configure
+--- coq-8.3-beta0-1/configure	2010-02-16 12:37:58.000000000 +0100
++++ coq-8.3-beta0-1-nix/configure	2010-05-11 17:47:44.000000000 +0200
+@@ -394,7 +394,6 @@ case $camldir_spec in
+ 	 ocamlyaccexec=$CAMLBIN/ocamlyacc
+ 	 ocamlmktopexec=$CAMLBIN/ocamlmktop
+ 	 ocamlmklibexec=$CAMLBIN/ocamlmklib
+-	 camlp4oexec=$CAMLBIN/camlp4o
+ esac
+ 
+ if test ! -f "$CAMLC" ; then
+@@ -626,7 +625,7 @@ case $COQIDE in
+             no)  LABLGTKLIB=+lablgtk2                   # Pour le message
+                  LABLGTKINCLUDES="-I $LABLGTKLIB";;     # Pour le makefile
+             yes) LABLGTKLIB="$lablgtkdir"               # Pour le message
+-                 LABLGTKINCLUDES="-I \"$LABLGTKLIB\"";; # Pour le makefile
++                 LABLGTKINCLUDES="-I $LABLGTKLIB";; # Pour le makefile
+         esac;;
+     no) LABLGTKINCLUDES="";;
+ esac
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 367e99223e78..a4a0a996b967 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -9209,6 +9209,11 @@ let
     camlp5 = camlp5_transitional;
   };
 
+  coq_beta = import ../applications/science/logic/coq/beta.nix {
+    inherit stdenv fetchurl ocaml lablgtk ncurses;
+    camlp5 = camlp5_transitional;
+  };
+
   hol_light = import ../applications/science/logic/hol_light {
     inherit stdenv fetchurl ocaml_with_sources;
   };