diff --git a/pkgs/applications/science/logic/coq/8.3rc1.nix b/pkgs/applications/science/logic/coq/8.3rc1.nix
index 4a549e5e93e9..66eb4de833e8 100644
--- a/pkgs/applications/science/logic/coq/8.3rc1.nix
+++ b/pkgs/applications/science/logic/coq/8.3rc1.nix
@@ -5,7 +5,7 @@
 {stdenv, fetchurl, ocaml, camlp5, lablgtk, ncurses}:
 
 stdenv.mkDerivation {
-  name = "coq8.3-8.3pre1";
+  name = "coq-devel-8.3pre1";
 
   src = fetchurl {
     url = http://coq.inria.fr/distrib/V8.3-rc1/files/coq-8.3-rc1.tar.gz;
@@ -40,7 +40,7 @@ stdenv.mkDerivation {
   buildFlags = "world"; # Debug with "world VERBOSE=1";
 
   meta = {
-    description = "Coq proof assistant";
+    description = "Coq proof assistant (development version)";
     longDescription = ''
       Coq is a formal proof management system.  It provides a formal language
       to write mathematical definitions, executable algorithms and theorems
diff --git a/pkgs/applications/science/logic/coq/beta.nix b/pkgs/applications/science/logic/coq/beta.nix
deleted file mode 100644
index c5c4221ac1ee..000000000000
--- a/pkgs/applications/science/logic/coq/beta.nix
+++ /dev/null
@@ -1,53 +0,0 @@
-# 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
deleted file mode 100644
index a5259eb43c08..000000000000
--- a/pkgs/applications/science/logic/coq/coq-8.3-beta0-1.patch
+++ /dev/null
@@ -1,20 +0,0 @@
-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 96d797122807..67cb13952a86 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -6675,11 +6675,7 @@ let
     camlp5 = camlp5_transitional;
   };
 
-  coq8_3 = callPackage ../applications/science/logic/coq/8.3rc1.nix {
-    camlp5 = camlp5_transitional;
-  };
-
-  coq_beta = callPackage ../applications/science/logic/coq/beta.nix {
+  coq_devel = callPackage ../applications/science/logic/coq/8.3rc1.nix {
     camlp5 = camlp5_transitional;
   };