diff --git a/pkgs/applications/science/logic/coq/8.3.nix b/pkgs/applications/science/logic/coq/8.3.nix
deleted file mode 100644
index 341267b2cebe..000000000000
--- a/pkgs/applications/science/logic/coq/8.3.nix
+++ /dev/null
@@ -1,82 +0,0 @@
-# - coqide compilation can be disabled by setting lablgtk to null;
-# - 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.
-
-{ stdenv, lib, make, fetchurl
-, ocaml, findlib, camlp5, ncurses, lablgtk ? null, csdp ? null }:
-
-assert lib.versionOlder ocaml.version "4";
-
-let 
-  version = "8.3pl4";
-  buildIde = lablgtk != null;
-  ideFlags = if buildIde then "-lablgtkdir ${lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt" else "";
-  idePatch = if buildIde then ''
-    substituteInPlace scripts/coqmktop.ml --replace \
-    "\"-I\"; \"+lablgtk2\"" \
-    "\"-I\"; \"$(echo "${lablgtk}"/lib/ocaml/*/site-lib/lablgtk2)\"; \"-I\"; \"$(echo "${lablgtk}"/lib/ocaml/*/site-lib/stublibs)\""
-  '' else "";
-  csdpPatch = if csdp != null then ''
-    substituteInPlace plugins/micromega/sos.ml --replace "; csdp" "; ${csdp}/bin/csdp"
-    substituteInPlace plugins/micromega/coq_micromega.ml --replace "System.search_exe_in_path \"csdp\"" "Some \"${csdp}/bin/csdp\""
-  '' else "";
-in
-
-stdenv.mkDerivation {
-  name = "coq-${version}";
-
-  src = fetchurl {
-    url = "https://coq.inria.fr/V${version}/files/coq-${version}.tar.gz";
-    sha256 = "17d3lmchmqir1rawnr52g78srg4wkd7clzpzfsivxc4y1zp6rwkr";
-  };
-
-  buildInputs = [ make ocaml findlib camlp5 ncurses lablgtk ];
-
-  prefixKey = "-prefix ";
-
-  preConfigure = ''
-    configureFlagsArray=(
-      -opt
-      -camldir ${ocaml}/bin
-      -camlp5dir $(ocamlfind query camlp5)
-      ${ideFlags}
-    )
-  '';
-
-  buildFlags = "world"; # Debug with "world VERBOSE=1";
-
-  patches = [ ./configure.8.3.patch ];
-
-  postPatch = ''
-    UNAME=$(type -tp uname)
-    RM=$(type -tp rm)
-    substituteInPlace configure --replace "/bin/uname" "$UNAME"
-    substituteInPlace tools/beautify-archive --replace "/bin/rm" "$RM"
-    ${idePatch}
-    ${csdpPatch}
-  '';
-
-  # This post install step is needed to build ssrcoqide from the ssreflect package
-  # It could be made optional, but I see little harm in including it in the default
-  # distribution -- roconnor
-  # This will likely no longer be necessary for coq >= 8.4. -- roconnor
-  postInstall = if buildIde then ''
-   cp ide/*.cmi ide/ide.*a $out/lib/coq/ide/
-  '' else "";
-
-  meta = with stdenv.lib; {
-    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 = licenses.lgpl21;
-    branch = "8.3";
-    maintainers = with maintainers; [ roconnor vbgl ];
-    platforms = with platforms; linux;
-  };
-}
diff --git a/pkgs/applications/science/logic/coq/configure.8.3.patch b/pkgs/applications/science/logic/coq/configure.8.3.patch
deleted file mode 100644
index 431cccac4b0b..000000000000
--- a/pkgs/applications/science/logic/coq/configure.8.3.patch
+++ /dev/null
@@ -1,1112 +0,0 @@
-diff -Nuar coq-8.3pl3-orig/configure coq-8.3pl3/configure
---- coq-8.3pl3-orig/configure	2011-12-19 22:57:30.000000000 +0100
-+++ coq-8.3pl3/configure	2012-03-17 16:38:16.000000000 +0100
-@@ -395,7 +395,6 @@
- 	 ocamlyaccexec=$CAMLBIN/ocamlyacc
- 	 ocamlmktopexec=$CAMLBIN/ocamlmktop
- 	 ocamlmklibexec=$CAMLBIN/ocamlmklib
--	 camlp4oexec=$CAMLBIN/camlp4o
- esac
- 
- if test ! -f "$CAMLC" ; then
-@@ -628,7 +627,7 @@
-             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 -Nuar coq-8.3pl3-orig/configure~ coq-8.3pl3/configure~
---- coq-8.3pl3-orig/configure~	1970-01-01 01:00:00.000000000 +0100
-+++ coq-8.3pl3/configure~	2011-12-19 22:57:30.000000000 +0100
-@@ -0,0 +1,1088 @@
-+#!/bin/sh
-+
-+##################################
-+#
-+#  Configuration script for Coq
-+# 
-+##################################
-+
-+VERSION=8.3pl3
-+VOMAGIC=08300
-+STATEMAGIC=58300
-+DATE=`LANG=C date +"%B %Y"`
-+
-+# Create the bin/ directory if non-existent
-+test -d bin || mkdir bin
-+
-+# a local which command for sh
-+which () {
-+IFS=":" # set words separator in PATH to be ':' (it allows spaces in dirnames)
-+for i in $PATH; do
-+  if test -z "$i"; then i=.; fi 
-+  if [ -f "$i/$1" ] ; then
-+	IFS=" "
-+        echo "$i/$1"
-+	break
-+  fi
-+done
-+}
-+
-+usage () {
-+    printf "Available options for configure are:\n"
-+    echo "-help"
-+    printf "\tDisplays this help page\n"
-+    echo "-prefix <dir>"
-+    printf "\tSet installation directory to <dir>\n"
-+    echo "-local"
-+    printf "\tSet installation directory to the current source tree\n"
-+    echo "-coqrunbyteflags"
-+    printf "\tSet link flags for VM-dependent bytecode (coqtop)\n"
-+    echo "-coqtoolsbyteflags"
-+    printf "\tSet link flags for VM-independant bytecode (coqdep, coqdoc, ...)\n"
-+    echo "-custom"
-+    printf "\tGenerate all bytecode executables with -custom (not recommended)\n"
-+    echo "-src"
-+    printf "\tSpecifies the source directory\n"
-+    echo "-bindir"
-+    echo "-libdir"
-+    echo "-mandir"
-+    echo "-docdir"
-+    printf "\tSpecifies where to install bin/lib/man/doc files resp.\n"
-+    echo "-emacslib"
-+    echo "-emacs"
-+    printf "\tSpecifies where emacs files are to be installed\n"
-+    echo "-coqdocdir"
-+    printf "\tSpecifies where Coqdoc style files are to be installed\n"
-+    echo "-camldir"
-+    printf "\tSpecifies the path to the OCaml library\n"
-+    echo "-lablgtkdir"
-+    printf "\tSpecifies the path to the Lablgtk library\n"
-+    echo "-camlp5dir"
-+    printf "\tSpecifies where to look for the Camlp5 library and tells to use it\n"
-+    echo "-arch"
-+    printf "\tSpecifies the architecture\n"
-+    echo "-opt"
-+    printf "\tSpecifies whether or not to use OCaml *.opt optimized compilers\n"
-+    echo "-natdynlink (yes|no)"
-+    printf "\tSpecifies whether or not to use dynamic loading of native code\n"
-+    echo "-coqide (opt|byte|no)"
-+    printf "\tSpecifies whether or not to compile Coqide\n"
-+    echo "-browser <command>"
-+    printf "\tUse <command> to open URL %%s\n"
-+    echo "-with-doc (yes|no)"
-+    printf "\tSpecifies whether or not to compile the documentation\n"
-+    echo "-with-geoproof (yes|no)"
-+    printf "\tSpecifies whether or not to use Geoproof binding\n"
-+    echo "-with-cc <file>"
-+    echo "-with-ar <file>"
-+    echo "-with-ranlib <file>"
-+    printf "\tTells configure where to find gcc/ar/ranlib executables\n"
-+    echo "-byte-only"
-+    printf "\tCompiles only bytecode version of Coq\n"
-+    echo "-debug"
-+    printf "\tAdd debugging information in the Coq executables\n"
-+    echo "-profile"
-+    printf "\tAdd profiling information in the Coq executables\n"
-+    echo "-annotate"
-+    printf "\tCompiles Coq with -dtypes option\n"
-+}
-+
-+
-+# Default OCaml binaries
-+bytecamlc=ocamlc
-+nativecamlc=ocamlopt
-+ocamlmklibexec=ocamlmklib
-+ocamlexec=ocaml
-+ocamldepexec=ocamldep
-+ocamldocexec=ocamldoc
-+ocamllexexec=ocamllex
-+ocamlyaccexec=ocamlyacc
-+ocamlmktopexec=ocamlmktop
-+camlp4oexec=camlp4o
-+
-+
-+coq_debug_flag=
-+coq_debug_flag_opt=
-+coq_profile_flag=
-+coq_annotate_flag=
-+best_compiler=opt
-+cflags="-fno-defer-pop -Wall -Wno-unused"
-+natdynlink=yes
-+
-+gcc_exec=gcc
-+ar_exec=ar
-+ranlib_exec=ranlib
-+
-+local=false
-+coqrunbyteflags_spec=no
-+coqtoolsbyteflags_spec=no
-+custom_spec=no
-+src_spec=no
-+prefix_spec=no
-+bindir_spec=no
-+libdir_spec=no
-+mandir_spec=no
-+docdir_spec=no
-+emacslib_spec=no
-+emacs_spec=no
-+camldir_spec=no
-+lablgtkdir_spec=no
-+coqdocdir_spec=no
-+arch_spec=no
-+coqide_spec=no
-+browser_spec=no
-+wwwcoq_spec=no
-+with_geoproof=false
-+with_doc=all
-+with_doc_spec=no
-+force_caml_version=no
-+force_caml_version_spec=no
-+
-+COQSRC=`pwd`
-+
-+# Parse command-line arguments
-+
-+while : ; do
-+  case "$1" in
-+    "") break;;
-+    -help|--help) usage
-+	          exit;;
-+    -prefix|--prefix) prefix_spec=yes
-+                      prefix="$2"
-+		      shift;;
-+    -local|--local) local=true;;
-+    -coqrunbyteflags|--coqrunbyteflags) coqrunbyteflags_spec=yes
-+                                        coqrunbyteflags="$2"
-+                                        shift;;
-+    -coqtoolsbyteflags|--coqtoolsbyteflags) coqtoolsbyteflags_spec=yes
-+                                            coqtoolsbyteflags="$2"
-+                                            shift;;
-+    -custom|--custom) custom_spec=yes
-+                      shift;;
-+    -src|--src) src_spec=yes
-+                COQSRC="$2"
-+	        shift;;
-+    -bindir|--bindir) bindir_spec=yes
-+                      bindir="$2"
-+		      shift;;
-+    -libdir|--libdir) libdir_spec=yes
-+                      libdir="$2"
-+		      shift;;
-+    -mandir|--mandir) mandir_spec=yes
-+                      mandir="$2"
-+		      shift;;
-+    -docdir|--docdir) docdir_spec=yes
-+                      docdir="$2"
-+		      shift;;
-+    -emacslib|--emacslib) emacslib_spec=yes
-+                          emacslib="$2"
-+			  shift;;
-+    -emacs |--emacs) emacs_spec=yes
-+		     emacs="$2"
-+		     shift;;
-+    -coqdocdir|--coqdocdir) coqdocdir_spec=yes
-+	              coqdocdir="$2"
-+		      shift;;
-+    -camldir|--camldir) camldir_spec=yes
-+	                camldir="$2"
-+			shift;;
-+    -lablgtkdir|--lablgtkdir) lablgtkdir_spec=yes
-+	                lablgtkdir="$2"
-+			shift;;
-+    -camlp5dir|--camlp5dir)
-+	                camlp5dir="$2"
-+			shift;;
-+    -arch|--arch) arch_spec=yes
-+                  arch=$2
-+		  shift;;
-+    -opt|--opt) bytecamlc=ocamlc.opt
-+                camlp4oexec=camlp4o  # can't add .opt since dyn load'll be required
-+                nativecamlc=ocamlopt.opt;;
-+    -natdynlink|--natdynlink) case "$2" in
-+	                  yes) natdynlink=yes;;
-+                          *) natdynlink=no
-+                        esac
-+                        shift;;
-+    -coqide|--coqide) coqide_spec=yes
-+		      case "$2" in
-+			  byte|opt) COQIDE=$2;;
-+			  *) COQIDE=no
-+		      esac
-+		      shift;;
-+    -browser|--browser) browser_spec=yes
-+		      BROWSER=$2
-+		      shift;;
-+    -coqwebsite|--coqwebsite) wwwcoq_spec=yes
-+                      WWWCOQ=$2
-+                      shift;;
-+    -with-doc|--with-doc) with_doc_spec=yes
-+		      case "$2" in
-+			  yes|all) with_doc=all;;
-+			  *) with_doc=no
-+		      esac
-+		      shift;;
-+    -with-geoproof|--with-geoproof) 
-+	  case "$2" in
-+	      yes) with_geoproof=true;;
-+	      no) with_geoproof=false;;
-+	  esac
-+	  shift;;
-+    -with-cc|-with-gcc|--with-cc|--with-gcc) 
-+	  gcc_spec=yes
-+	  gcc_exec=$2
-+	  shift;;
-+    -with-ar|--with-ar) 
-+	  ar_spec=yes
-+	  ar_exec=$2
-+	  shift;;
-+    -with-ranlib|--with-ranlib) 
-+	  ranlib_spec=yes
-+	  ranlib_exec=$2
-+	  shift;;
-+    -byte-only|-byteonly|--byteonly|--byte-only) best_compiler=byte;;
-+    -debug|--debug) coq_debug_flag=-g;;
-+    -profile|--profile) coq_profile_flag=-p;;
-+    -annotate|--annotate) coq_annotate_flag=-dtypes;;
-+    -force-caml-version|--force-caml-version|-force-ocaml-version|--force-ocaml-version) 
-+          force_caml_version_spec=yes
-+	  force_caml_version=yes;;
-+    *) echo "Unknown option \"$1\"." 1>&2; usage; exit 2;;
-+  esac
-+  shift
-+done
-+
-+if [ $prefix_spec = yes -a $local = true ] ; then
-+  echo "Options -prefix and -local are incompatible."
-+  echo "Configure script failed!"
-+  exit 1
-+fi
-+
-+# compile date
-+DATEPGM=`which date`
-+case $DATEPGM in
-+    "") echo "I can't find the program \"date\" in your path."
-+        echo "Please give me the current date"
-+	read COMPILEDATE;;
-+    *)  COMPILEDATE=`date +"%h %d %Y %H:%M:%S"`;;
-+esac
-+
-+# Architecture
-+
-+case $arch_spec in
-+    no) 
-+    # First we test if we are running a Cygwin system
-+    if [ `uname -s | cut -c -6` = "CYGWIN" ] ; then
-+	ARCH="win32"
-+    else
-+	# If not, we determine the architecture
-+	if test -x /bin/arch ; then
-+ 	    ARCH=`/bin/arch`
-+ 	elif test -x /usr/bin/arch ; then
-+ 	    ARCH=`/usr/bin/arch`
-+ 	elif test -x /usr/ucb/arch ; then
-+ 	    ARCH=`/usr/ucb/arch`
-+ 	elif test -x /bin/uname ; then
-+ 	    ARCH=`/bin/uname -s`
-+ 	elif test -x /usr/bin/uname ; then
-+ 	    ARCH=`/usr/bin/uname -s`
-+	else
-+	    echo "I can not automatically find the name of your architecture."
-+	    printf "%s"\
-+		"Give me a name, please [win32 for Win95, Win98 or WinNT]: "
-+	    read ARCH
-+	fi
-+    fi;;
-+    yes) ARCH=$arch
-+esac
-+
-+# executable extension
-+
-+case $ARCH in
-+    win32) 
-+      EXE=".exe"
-+      DLLEXT=".dll";;
-+    *) EXE=""
-+       DLLEXT=".so"
-+esac
-+
-+# Is the source tree checked out from a recognised
-+# version control system ?
-+if test -e .svn/entries ; then 
-+    checkedout=svn
-+elif [ -d '{arch}' ]; then
-+    checkedout=gnuarch
-+elif [ -z "${GIT_DIR}" ] && [ -d .git ] || [ -d "${GIT_DIR}" ]; then
-+    checkedout=git
-+else
-+    checkedout=0
-+fi
-+
-+# make command
-+
-+MAKE=`which make`
-+if [ "$MAKE" != "" ]; then
-+  MAKEVERSION=`$MAKE -v | head -1 | cut -d" " -f3`
-+  MAKEVERSIONMAJOR=`echo $MAKEVERSION | cut -d. -f1`
-+  MAKEVERSIONMINOR=`echo $MAKEVERSION | cut -d. -f2`
-+  if [ "$MAKEVERSIONMAJOR" -eq 3 -a "$MAKEVERSIONMINOR" -ge 81 ]; then
-+      echo "You have GNU Make $MAKEVERSION. Good!"
-+  else
-+      OK="no"
-+      if [ -x ./make ]; then
-+	  MAKEVERSION=`./make -v | head -1`
-+	  if [ "$MAKEVERSION" = "GNU Make 3.81" ]; then OK="yes"; fi
-+      fi
-+      if [ $OK = "no" ]; then
-+	  echo "GNU Make >= 3.81 is needed."
-+	  echo "Make 3.81 can be downloaded from ftp://ftp.gnu.org/gnu/make/make-3.81.tar.gz"
-+	  echo "then locally installed on a Unix-style system by issuing:"
-+	  echo "  tar xzvf make-3.81.tar.gz"
-+	  echo "  cd make-3.81"
-+          echo "  ./configure"
-+          echo "  make"
-+          echo "  mv make .."
-+	  echo "  cd .."
-+	  echo "Restart then the configure script and later use ./make instead of make."
-+	  exit 1
-+      else
-+	  echo "You have locally installed GNU Make 3.81. Good!"
-+      fi
-+  fi
-+else
-+  echo "Cannot find GNU Make >= 3.81."
-+fi
-+
-+# Browser command
-+
-+if [ "$browser_spec" = "no" ]; then
-+    case $ARCH in
-+        win32) BROWSER='C:\PROGRA~1\INTERN~1\IEXPLORE %s' ;;
-+        *) BROWSER='firefox -remote "OpenURL(%s,new-tab)" || firefox %s &' ;;
-+    esac
-+fi
-+
-+if [ "$wwwcoq_spec" = "no" ]; then
-+    WWWCOQ="http://coq.inria.fr/"
-+fi
-+
-+#########################################
-+# Objective Caml programs
-+
-+case $camldir_spec in
-+    no) CAMLC=`which $bytecamlc`
-+	case "$CAMLC" in
-+	    "") echo "$bytecamlc is not present in your path!"
-+		echo "Give me manually the path to the $bytecamlc executable [/usr/local/bin by default]: "
-+		read CAMLC
-+		
-+		case "$CAMLC" in
-+		    "") CAMLC=/usr/local/bin/$bytecamlc;;
-+		    */ocamlc|*/ocamlc.opt) true;;
-+		    */) CAMLC="${CAMLC}"$bytecamlc;;
-+		    *) CAMLC="${CAMLC}"/$bytecamlc;;
-+		esac
-+	esac
-+	CAMLBIN=`dirname "$CAMLC"`;;
-+    yes) CAMLC=$camldir/$bytecamlc
-+        
-+         CAMLBIN=`dirname "$CAMLC"`
-+	 bytecamlc="$CAMLC"
-+	 nativecamlc=$CAMLBIN/$nativecamlc
-+	 ocamlexec=$CAMLBIN/ocaml
-+	 ocamldepexec=$CAMLBIN/ocamldep
-+	 ocamldocexec=$CAMLBIN/ocamldoc
-+	 ocamllexexec=$CAMLBIN/ocamllex
-+	 ocamlyaccexec=$CAMLBIN/ocamlyacc
-+	 ocamlmktopexec=$CAMLBIN/ocamlmktop
-+	 ocamlmklibexec=$CAMLBIN/ocamlmklib
-+	 camlp4oexec=$CAMLBIN/camlp4o
-+esac
-+
-+if test ! -f "$CAMLC" ; then
-+    echo "I can not find the executable '$CAMLC'. Have you installed it?"
-+    echo "Configuration script failed!"
-+    exit 1
-+fi
-+
-+# Under Windows, OCaml only understands Windows filenames (C:\...)
-+case $ARCH in
-+    win32) CAMLBIN=`cygpath -m ${CAMLBIN}`;;
-+esac
-+
-+CAMLVERSION=`"$bytecamlc" -version`
-+
-+case $CAMLVERSION in
-+    1.*|2.*|3.00|3.01|3.02|3.03|3.03alpha|3.04|3.05beta|3.05|3.06|3.07*|3.08*|3.09*)
-+	echo "Your version of Objective-Caml is $CAMLVERSION."
-+	if [ "$force_caml_version" = "yes" ]; then
-+	    echo "*Warning* You are compiling Coq with an outdated version of Objective-Caml."
-+	else
-+	    echo "          You need Objective-Caml 3.10.2 or later."
-+	    echo "          Configuration script failed!"
-+	    exit 1
-+	fi;;
-+    ?*)
-+	CAMLP4COMPAT="-loc loc" 
-+	echo "You have Objective-Caml $CAMLVERSION. Good!";;
-+    *)
-+	echo "I found the Objective-Caml compiler but cannot find its version number!"
-+	echo "Is it installed properly?"
-+	echo "Configuration script failed!"
-+	exit 1;;
-+esac
-+
-+CAMLTAG=OCAML`echo $CAMLVERSION | sed -e "s/\([1-9]\)\.\([0-9]*\).*/\1\2/g"`
-+
-+# For coqmktop & bytecode compiler
-+
-+case $ARCH in
-+    win32) # Awfull trick to get around a ^M problem at the end of CAMLLIB
-+      CAMLLIB=`"$CAMLC" -where | sed -e 's/^\(.*\)$/\1/'` ;;
-+    *)
-+      CAMLLIB=`"$CAMLC" -where`
-+esac
-+
-+if [ "$coq_debug_flag" = "-g" ]; then
-+    case $CAMLTAG in
-+        OCAML31*)
-+            # Compilation debug flag
-+            coq_debug_flag_opt="-g"
-+            ;;
-+    esac
-+fi
-+
-+# Native dynlink
-+if [ "$natdynlink" = "yes" -a -f `"$CAMLC" -where`/dynlink.cmxa ]; then
-+    HASNATDYNLINK=true
-+else
-+    HASNATDYNLINK=false
-+fi
-+
-+case $HASNATDYNLINK,`uname -s`,`uname -r`,$CAMLVERSION in
-+    true,Darwin,9.*,3.11.*)  # ocaml 3.11.0 dynlink on MacOS 10.5 is buggy
-+        NATDYNLINKFLAG=os5fixme;;
-+    #Possibly a problem on 10.6.0/10.6.1/10.6.2
-+    #May just be a 32 vs 64 problem for all 10.6.*
-+    true,Darwin,10.0.*,3.11.*) # Possibly a problem on 10.6.0
-+        NATDYNLINKFLAG=os5fixme;;
-+    true,Darwin,10.1.*,3.11.*) # Possibly a problem on 10.6.1
-+        NATDYNLINKFLAG=os5fixme;;
-+    true,Darwin,10.2.*,3.11.*) # Possibly a problem on 10.6.2
-+        NATDYNLINKFLAG=os5fixme;;
-+    true,Darwin,10.*,3.11.*)
-+        if [ `getconf LONG_BIT` = "32" ]; then
-+	    # Still a problem for x86_32
-+            NATDYNLINKFLAG=os5fixme
-+        else
-+	    # Not a problem for x86_64
-+            NATDYNLINKFLAG=$HASNATDYNLINK
-+        fi;;
-+    *)
-+        NATDYNLINKFLAG=$HASNATDYNLINK;;
-+esac
-+
-+# Camlp4 / Camlp5 configuration
-+
-+if [ "$camlp5dir" != "" ]; then
-+    CAMLP4=camlp5
-+    CAMLP4LIB=$camlp5dir
-+    if [ ! -f $camlp5dir/camlp5.cma ]; then
-+	echo "Cannot find camlp5 libraries in $camlp5dir (camlp5.cma not found)."
-+	echo "Configuration script failed!"
-+	exit 1
-+    fi
-+    camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'`
-+else
-+    case $CAMLTAG in
-+        OCAML31*)
-+            if [ -x "${CAMLLIB}/camlp5" ]; then
-+                CAMLP4LIB=+camlp5
-+            elif [ -x "${CAMLLIB}/site-lib/camlp5" ]; then
-+                CAMLP4LIB=+site-lib/camlp5
-+            else
-+	        echo "Objective Caml $CAMLVERSION found but no Camlp5 installed."
-+	        echo "Configuration script failed!"
-+	        exit 1
-+            fi
-+            CAMLP4=camlp5
-+            camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'`
-+            ;;
-+        *)
-+            CAMLP4=camlp4
-+            CAMLP4LIB=+camlp4
-+            ;;
-+    esac
-+fi
-+
-+if [ "$CAMLP4" = "camlp5" ] && `$camlp4oexec -v 2>&1 | grep -q 5.00`; then
-+    echo "Camlp5 version 5.00 not supported: versions 4.0x or >= 5.01 are OK"
-+    echo "(depending also on your ocaml version)."
-+    echo "Configuration script failed!"
-+    exit 1
-+fi
-+
-+
-+case $CAMLP4LIB in
-+    +*) FULLCAMLP4LIB=$CAMLLIB/`echo $CAMLP4LIB | cut -b 2-`;;
-+    *)  FULLCAMLP4LIB=$CAMLP4LIB;;
-+esac
-+
-+# Assume that camlp(4|5) binaries are at the same place as ocaml ones
-+# (this should become configurable some day) 
-+CAMLP4BIN=${CAMLBIN}
-+
-+# do we have a native compiler: test of ocamlopt and its version
-+
-+if [ "$best_compiler" = "opt" ] ; then
-+  if test -e "$nativecamlc" || test -e "`which $nativecamlc`"; then
-+      CAMLOPTVERSION=`"$nativecamlc" -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' `
-+      if [ "`uname -s`" = "Darwin" -a "$ARCH" = "i386" ]; then
-+	  case $CAMLOPTVERSION in
-+	      3.09.3|3.1?*) ;;
-+	      *) echo "Native compilation on MacOS X Pentium requires Objective-Caml >= 3.09.3,"
-+		 best_compiler=byte
-+		 echo "only the bytecode version of Coq will be available."
-+	  esac
-+      elif [ ! -f $FULLCAMLP4LIB/gramlib.cmxa ]; then
-+	  best_compiler=byte
-+	  echo "Cannot find native-code $CAMLP4,"
-+	  echo "only the bytecode version of Coq will be available."
-+      else
-+        if [ "$CAMLOPTVERSION" != "$CAMLVERSION" ] ; then
-+	  echo "Native and bytecode compilers do not have the same version!"
-+        fi
-+        echo "You have native-code compilation. Good!"
-+      fi
-+  else
-+      best_compiler=byte
-+      echo "You have only bytecode compilation."
-+  fi
-+fi
-+
-+# OS dependent libraries
-+
-+case $ARCH in
-+  sun4*) OS=`uname -r`
-+	case $OS in
-+	   5*) OS="Sun Solaris $OS"
-+	       OSDEPLIBS="-cclib -lunix -cclib -lnsl -cclib -lsocket";;
-+	   *) OS="Sun OS $OS"
-+	      OSDEPLIBS="-cclib -lunix"
-+        esac;;
-+  alpha) OSDEPLIBS="-cclib -lunix";;
-+  win32) OS="Win32" 
-+	 OSDEPLIBS="-cclib -lunix"
-+	 cflags="-mno-cygwin $cflags";;
-+  *) OSDEPLIBS="-cclib -lunix"
-+esac
-+
-+# lablgtk2 and CoqIDE
-+
-+# -byte-only should imply -coqide byte, unless the user decides otherwise
-+
-+if [ "$best_compiler" = "byte" -a "$coqide_spec" = "no" ]; then 
-+    coqide_spec=yes
-+    COQIDE=byte
-+fi
-+
-+# Which coqide is asked ? which one is possible ?
-+
-+if [ "$coqide_spec" = "yes" -a "$COQIDE" = "no" ]; then 
-+    echo "CoqIde disabled as requested."
-+else
-+    case $lablgtkdir_spec in
-+	no) 
-+	    if [ -f "${CAMLLIB}/lablgtk2/glib.mli" ]; then
-+		lablgtkdir=${CAMLLIB}/lablgtk2
-+	    elif [ -f "${CAMLLIB}/site-lib/lablgtk2/glib.mli" ]; then
-+		lablgtkdir=${CAMLLIB}/site-lib/lablgtk2
-+	    fi;;
-+	yes)
-+	    if [ ! -f "$lablgtkdir/glib.mli" ]; then
-+		echo "Incorrect LablGtk2 library (glib.mli not found)."
-+		echo "Configuration script failed!"
-+		exit 1
-+	    fi;;
-+    esac
-+    if [ "$lablgtkdir" = "" ]; then
-+	echo "LablGtk2 not found: CoqIde will not be available."
-+	COQIDE=no
-+    elif [ -z "`grep -w convert_with_fallback "$lablgtkdir/glib.mli"`" ]; then
-+	echo "LablGtk2 found but too old: CoqIde will not be available."
-+	COQIDE=no;
-+    elif [ "$coqide_spec" = "yes" -a "$COQIDE" = "byte" ]; then 
-+	echo "LablGtk2 found, bytecode CoqIde will be used as requested."
-+	COQIDE=byte
-+    elif [ ! -f "${CAMLLIB}/threads/threads.cmxa" ]; then 
-+	echo "LablGtk2 found, no native threads: bytecode CoqIde will be available."
-+	COQIDE=byte
-+    else 
-+	echo "LablGtk2 found, native threads: native CoqIde will be available."
-+	COQIDE=opt
-+    fi
-+fi
-+
-+case $COQIDE in
-+    byte|opt)
-+        case $lablgtkdir_spec 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
-+        esac;;
-+    no) LABLGTKINCLUDES="";;
-+esac
-+
-+# strip command
-+
-+case $ARCH in
-+    win32)
-+	# true -> strip : it exists under cygwin !
-+	STRIPCOMMAND="strip";; 
-+    *)
-+    if [ "$coq_profile_flag" = "-p" ] || [ "$coq_debug_flag" = "-g" ] ||
-+       [ "`uname -s`" = "Darwin" -a "$HASNATDYNLINK" = "true" ]
-+    then
-+	STRIPCOMMAND="true"
-+    else
-+	STRIPCOMMAND="strip"
-+    fi
-+esac
-+
-+# mktexlsr
-+#MKTEXLSR=`which mktexlsr`
-+#case $MKTEXLSR in
-+#    "") MKTEXLSR=true;;
-+#esac
-+
-+# "
-+### Test if documentation can be compiled (latex, hevea)
-+
-+if test "$with_doc" = "all" 
-+then
-+    for cmd in "latex" "hevea" ; do
-+	if test ! -x "`which $cmd`"
-+	then 
-+	    echo "$cmd was not found; documentation will not be available"
-+	    with_doc=no
-+	    break
-+	fi
-+    done
-+fi
-+
-+###########################################
-+# bindir, libdir, mandir, docdir, etc.
-+
-+case $src_spec in
-+  no) COQTOP=${COQSRC}
-+esac
-+
-+# OCaml only understand Windows filenames (C:\...)
-+case $ARCH in
-+    win32) COQTOP=`cygpath -m ${COQTOP}`
-+esac
-+
-+case $ARCH in
-+  win32)
-+	 bindir_def='C:\coq\bin'
-+	 libdir_def='C:\coq\lib'
-+	 mandir_def='C:\coq\man'
-+	 docdir_def='C:\coq\doc'
-+	 emacslib_def='C:\coq\emacs'
-+         coqdocdir_def='C:\coq\latex';;
-+  *)
-+	 bindir_def=/usr/local/bin
-+	 libdir_def=/usr/local/lib/coq
-+	 mandir_def=/usr/local/man
-+	 docdir_def=/usr/local/share/doc/coq
-+	 emacslib_def=/usr/local/share/emacs/site-lisp
-+         coqdocdir_def=/usr/local/share/texmf/tex/latex/misc;;
-+esac
-+
-+emacs_def=emacs
-+
-+case $bindir_spec/$prefix_spec/$local in
-+    yes/*/*) BINDIR=$bindir ;;
-+    */yes/*) BINDIR=$prefix/bin ;;
-+    */*/true) BINDIR=$COQTOP/bin ;;
-+    *) printf "Where should I install the Coq binaries [$bindir_def]? "
-+        read BINDIR
-+	case $BINDIR in
-+	    "") BINDIR=$bindir_def;;
-+	    *) true;;
-+	esac;;
-+esac
-+
-+case $libdir_spec/$prefix_spec/$local in
-+    yes/*/*) LIBDIR=$libdir;;
-+    */yes/*)
-+        case $ARCH in
-+          win32) LIBDIR=$prefix ;;
-+          *)  LIBDIR=$prefix/lib/coq ;;
-+        esac ;;
-+    */*/true) LIBDIR=$COQTOP ;;
-+    *)  printf "Where should I install the Coq library [$libdir_def]? "
-+        read LIBDIR
-+	case $LIBDIR in
-+	    "") LIBDIR=$libdir_def;;
-+	    *) true;;
-+	esac;;
-+esac
-+
-+case $mandir_spec/$prefix_spec/$local in
-+    yes/*/*) MANDIR=$mandir;;
-+    */yes/*) MANDIR=$prefix/man ;;
-+    */*/true) MANDIR=$COQTOP/man ;;
-+    *)  printf "Where should I install the Coq man pages [$mandir_def]? "
-+        read MANDIR
-+	case $MANDIR in
-+	    "") MANDIR=$mandir_def;;
-+	    *) true;;
-+	esac;;
-+esac
-+
-+case $docdir_spec/$prefix_spec/$local in
-+    yes/*/*) DOCDIR=$docdir; HTMLREFMANDIR=$DOCDIR/html/refman;;
-+    */yes/*) DOCDIR=$prefix/share/doc/coq; HTMLREFMANDIR=$DOCDIR/html/refman;;
-+    */*/true) DOCDIR=$COQTOP/doc; HTMLREFMANDIR=$DOCDIR/refman/html;;
-+    *)  printf "Where should I install the Coq documentation [$docdir_def]? "
-+        read DOCDIR
-+	case $DOCDIR in
-+	    "") DOCDIR=$docdir_def; HTMLREFMANDIR=$DOCDIR/html/refman;;
-+	    *) true;;
-+	esac;;
-+esac
-+
-+case $emacslib_spec/$prefix_spec/$local in
-+    yes/*/*) EMACSLIB=$emacslib;;
-+    */yes/*)
-+        case $ARCH in
-+          win32) EMACSLIB=$prefix/emacs ;;
-+          *)  EMACSLIB=$prefix/share/emacs/site-lisp ;;
-+        esac ;;
-+    */*/true) EMACSLIB=$COQTOP/tools/emacs ;;
-+    *) printf "Where should I install the Coq Emacs mode [$emacslib_def]? "
-+        read EMACSLIB
-+	case $EMACSLIB in
-+	    "") EMACSLIB=$emacslib_def;;
-+	    *) true;;
-+	esac;;
-+esac
-+
-+case $coqdocdir_spec/$prefix_spec/$local in
-+    yes/*/*) COQDOCDIR=$coqdocdir;;
-+    */yes/*)
-+        case $ARCH in
-+          win32) COQDOCDIR=$prefix/latex ;;
-+          *)  COQDOCDIR=$prefix/share/emacs/site-lisp ;;
-+        esac ;;
-+    */*/true) COQDOCDIR=$COQTOP/tools/coqdoc ;;
-+    *) printf "Where should I install Coqdoc TeX/LaTeX files [$coqdocdir_def]? "
-+        read COQDOCDIR
-+	case $COQDOCDIR in
-+	    "") COQDOCDIR=$coqdocdir_def;;
-+	    *) true;;
-+	esac;;
-+esac
-+
-+# Determine if we enable -custom by default (Windows and MacOS)
-+CUSTOM_OS=no
-+if [ "$ARCH" = "win32" ] || [ "`uname -s`" = "Darwin" ]; then
-+    CUSTOM_OS=yes
-+fi
-+
-+BUILDLDPATH="# you might want to set CAML_LD_LIBRARY_PATH by hand!"
-+case $coqrunbyteflags_spec/$local/$custom_spec/$CUSTOM_OS in
-+    yes/*/*/*) COQRUNBYTEFLAGS="$coqrunbyteflags";;
-+    */*/yes/*|*/*/*/yes) COQRUNBYTEFLAGS="-custom";;
-+    */true/*/*) COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath '$COQTOP'/kernel/byterun";;
-+    *)
-+        COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath '$LIBDIR'"
-+        BUILDLDPATH="export CAML_LD_LIBRARY_PATH='$COQTOP'/kernel/byterun";;
-+esac
-+case $coqtoolsbyteflags_spec/$custom_spec/$CUSTOM_OS in
-+    yes/*/*) COQTOOLSBYTEFLAGS="$coqtoolsbyteflags";;
-+    */yes/*|*/*/yes) COQTOOLSBYTEFLAGS="-custom";;
-+    *) COQTOOLSBYTEFLAGS="";;
-+esac
-+
-+# case $emacs_spec in
-+#     no) printf "Which Emacs command should I use to compile coq.el [$emacs_def]? "
-+#         read EMACS
-+	
-+# 	case $EMACS in
-+# 	    "") EMACS=$emacs_def;;
-+# 	    *) true;;
-+# 	esac;;
-+#     yes) EMACS=$emacs;;
-+# esac
-+
-+
-+
-+###########################################
-+# Summary of the configuration
-+
-+echo ""
-+echo "  Coq top directory                 : $COQTOP"
-+echo "  Architecture                      : $ARCH"
-+if test ! -z "$OS" ; then
-+  echo "  Operating system                  : $OS"
-+fi
-+echo "  Coq VM bytecode link flags        : $COQRUNBYTEFLAGS"
-+echo "  Coq tools bytecode link flags     : $COQTOOLSBYTEFLAGS"
-+echo "  OS dependent libraries            : $OSDEPLIBS"
-+echo "  Objective-Caml/Camlp4 version     : $CAMLVERSION"
-+echo "  Objective-Caml/Camlp4 binaries in : $CAMLBIN"
-+echo "  Objective-Caml library in         : $CAMLLIB"
-+echo "  Camlp4 library in                 : $CAMLP4LIB"
-+if test "$best_compiler" = opt ; then
-+echo "  Native dynamic link support       : $HASNATDYNLINK"
-+fi
-+if test "$COQIDE" != "no"; then
-+echo "  Lablgtk2 library in               : $LABLGTKLIB"
-+fi
-+if test "$with_doc" = "all"; then
-+echo "  Documentation                     : All"
-+else
-+echo "  Documentation                     : None"
-+fi
-+echo "  CoqIde                            : $COQIDE"
-+echo "  Web browser                       : $BROWSER"
-+echo "  Coq web site                      : $WWWCOQ"
-+echo ""
-+
-+echo "  Paths for true installation:"
-+echo "    binaries      will be copied in $BINDIR"
-+echo "    library       will be copied in $LIBDIR"
-+echo "    man pages     will be copied in $MANDIR"
-+echo "    documentation will be copied in $DOCDIR"
-+echo "    emacs mode    will be copied in $EMACSLIB"
-+echo ""
-+
-+##################################################
-+# Building the $COQTOP/dev/ocamldebug-coq file
-+##################################################
-+
-+OCAMLDEBUGCOQ=$COQSRC/dev/ocamldebug-coq
-+
-+if test "$coq_debug_flag" = "-g" ; then
-+  rm -f $OCAMLDEBUGCOQ
-+  sed -e "s|COQTOPDIRECTORY|$COQTOP|" \
-+      -e "s|COQLIBDIRECTORY|$LIBDIR|" \
-+      -e "s|CAMLBINDIRECTORY|$CAMLBIN|" \
-+      -e "s|CAMLP4LIBDIRECTORY|$FULLCAMLP4LIB|"\
-+      $OCAMLDEBUGCOQ.template > $OCAMLDEBUGCOQ
-+  chmod a-w,a+x $OCAMLDEBUGCOQ
-+fi
-+
-+####################################################
-+# Fixing lablgtk types (before/after 2.6.0) 
-+####################################################
-+
-+if [ ! "$COQIDE" = "no" ]; then 
-+    if grep "class view " "$lablgtkdir/gText.mli" | grep -q "\[>" ; then
-+       if grep -q "?accepts_tab:bool" "$lablgtkdir/gText.mli" ; then
-+        cp -f ide/undo_lablgtk_ge212.mli ide/undo.mli
-+       else
-+	cp -f ide/undo_lablgtk_ge26.mli ide/undo.mli
-+       fi
-+    else
-+	cp -f ide/undo_lablgtk_lt26.mli ide/undo.mli
-+    fi
-+fi  
-+
-+##############################################
-+# Creation of configuration files
-+##############################################
-+
-+mlconfig_file="$COQSRC/config/coq_config.ml"
-+config_file="$COQSRC/config/Makefile"
-+config_template="$COQSRC/config/Makefile.template"
-+
-+
-+### Warning !!
-+### After this line, be careful when using variables,
-+### since some of them (e.g. $COQSRC) will be escaped
-+
-+
-+# An escaped version of a variable
-+escape_var () {
-+"$ocamlexec" 2>&1 1>/dev/null <<EOF
-+  prerr_endline(String.escaped(Sys.getenv"$VAR"));;
-+EOF
-+}
-+
-+# Escaped version of browser command
-+export BROWSER
-+BROWSER=`VAR=BROWSER escape_var`
-+
-+# damned backslashes under M$Windows
-+case $ARCH in
-+    win32)
-+	COQTOP=`echo $COQTOP |sed -e 's|\\\|\\\\\\\|g'`
-+	BINDIR=`echo $BINDIR |sed -e 's|\\\|\\\\\\\|g'`
-+	COQSRC=`cygpath -m $COQSRC |sed -e 's|\\\|\\\\\\\|g'`
-+	LIBDIR=`echo $LIBDIR |sed -e 's|\\\|\\\\\\\|g'`
-+	CAMLBIN=`echo $CAMLBIN |sed -e 's|\\\|\\\\\\\|g'`
-+	CAMLLIB=`echo $CAMLLIB |sed -e 's|\\\|\\\\\\\|g'`
-+	MANDIR=`echo $MANDIR |sed -e 's|\\\|\\\\\\\|g'`
-+	DOCDIR=`echo $DOCDIR |sed -e 's|\\\|\\\\\\\|g'`
-+	EMACSLIB=`echo $EMACSLIB |sed -e 's|\\\|\\\\\\\|g'`
-+	COQDOCDIR=`echo $COQDOCDIR |sed -e 's|\\\|\\\\\\\|g'`
-+	CAMLP4BIN=`echo $CAMLP4BIN |sed -e 's|\\\|\\\\\\\|g'`
-+	CAMLP4LIB=`echo $CAMLP4LIB |sed -e 's|\\\|\\\\\\\|g'`
-+	LABLGTKINCLUDES=`echo $LABLGTKINCLUDES |sed -e 's|\\\|\\\\\\\|g'`
-+	COQRUNBYTEFLAGS=`echo $COQRUNBYTEFLAGS |sed -e 's|\\\|\\\\\\\|g'`
-+	COQTOOLSBYTEFLAGS=`echo $COQTOOLSBYTEFLAGS |sed -e 's|\\\|\\\\\\\|g'`
-+	BUILDLDPATH=`echo $BUILDLDPATH |sed -e 's|\\\|\\\\\\\|g'`
-+	ocamlexec=`echo $ocamlexec |sed -e 's|\\\|\\\\\\\|g'`
-+	bytecamlc=`echo $bytecamlc |sed -e 's|\\\|\\\\\\\|g'`
-+	nativecamlc=`echo $nativecamlc |sed -e 's|\\\|\\\\\\\|g'`
-+	ocamlmklibexec=`echo $ocamlmklibexec |sed -e 's|\\\|\\\\\\\|g'`
-+	ocamldepexec=`echo $ocamldepexec |sed -e 's|\\\|\\\\\\\|g'`
-+	ocamldocexec=`echo $ocamldocexec |sed -e 's|\\\|\\\\\\\|g'`
-+	ocamllexexec=`echo $ocamllexexec |sed -e 's|\\\|\\\\\\\|g'`
-+	ocamlyaccexec=`echo $ocamlyaccexec |sed -e 's|\\\|\\\\\\\|g'`
-+	camlp4oexec=`echo $camlp4oexec |sed -e 's|\\\|\\\\\\\|g'`
-+    ;;
-+esac
-+
-+#####################################################
-+# Building the $COQTOP/config/coq_config.ml file
-+#####################################################
-+
-+rm -f "$mlconfig_file"
-+cat << END_OF_COQ_CONFIG > $mlconfig_file
-+(* DO NOT EDIT THIS FILE: automatically generated by ../configure *)
-+
-+let local = $local
-+let coqrunbyteflags = "$COQRUNBYTEFLAGS"
-+let coqlib = "$LIBDIR"
-+let coqsrc = "$COQSRC"
-+let ocaml = "$ocamlexec"
-+let ocamlc = "$bytecamlc"
-+let ocamlopt = "$nativecamlc"
-+let ocamlmklib = "$ocamlmklibexec"
-+let ocamldep = "$ocamldepexec"
-+let ocamldoc = "$ocamldocexec"
-+let ocamlyacc = "$ocamlyaccexec"
-+let ocamllex = "$ocamllexexec"
-+let camlbin = "$CAMLBIN"
-+let camllib = "$CAMLLIB"
-+let camlp4 = "$CAMLP4"
-+let camlp4o = "$camlp4oexec"
-+let camlp4bin = "$CAMLP4BIN"
-+let camlp4lib = "$CAMLP4LIB"
-+let camlp4compat = "$CAMLP4COMPAT"
-+let coqideincl = "$LABLGTKINCLUDES"
-+let cflags = "$cflags"
-+let best = "$best_compiler"
-+let arch = "$ARCH"
-+let has_coqide = "$COQIDE"
-+let has_natdynlink = $HASNATDYNLINK
-+let natdynlinkflag = "$NATDYNLINKFLAG"
-+let osdeplibs = "$OSDEPLIBS"
-+let version = "$VERSION"
-+let caml_version = "$CAMLVERSION"
-+let date = "$DATE"
-+let compile_date = "$COMPILEDATE"
-+let vo_magic_number = $VOMAGIC
-+let state_magic_number = $STATEMAGIC
-+let exec_extension = "$EXE"
-+let with_geoproof = ref $with_geoproof
-+let browser = "$BROWSER"
-+let wwwcoq = "$WWWCOQ"
-+let wwwrefman = wwwcoq ^ "distrib/" ^ version ^ "/refman/"
-+let wwwstdlib = wwwcoq ^ "distrib/" ^ version ^ "/stdlib/"
-+let localwwwrefman = "file://$HTMLREFMANDIR/"
-+
-+END_OF_COQ_CONFIG
-+
-+# to be sure printf is found on windows when spaces occur in PATH variable
-+PRINTF=`which printf`
-+
-+# Subdirectories of theories/ added in coq_config.ml
-+subdirs () {
-+    (cd $1; find * \( -name .svn -prune \) -o \( -type d -exec $PRINTF "\"%s\";\n" {} \; \) >> "$mlconfig_file")
-+}
-+
-+echo "let theories_dirs = [" >> "$mlconfig_file"
-+subdirs theories
-+echo "]" >> "$mlconfig_file"
-+
-+echo "let plugins_dirs = [" >> "$mlconfig_file"
-+subdirs plugins
-+echo "]" >> "$mlconfig_file"
-+
-+chmod a-w "$mlconfig_file"
-+
-+
-+###############################################
-+# Building the $COQTOP/config/Makefile file
-+###############################################
-+
-+rm -f "$config_file"
-+
-+sed -e "s|LOCALINSTALLATION|$local|" \
-+    -e "s|XCOQRUNBYTEFLAGS|$COQRUNBYTEFLAGS|" \
-+    -e "s|XCOQTOOLSBYTEFLAGS|$COQTOOLSBYTEFLAGS|" \
-+    -e "s|COQSRCDIRECTORY|$COQSRC|" \
-+    -e "s|COQVERSION|$VERSION|" \
-+    -e "s|BINDIRDIRECTORY|$BINDIR|" \
-+    -e "s|COQLIBDIRECTORY|$LIBDIR|" \
-+    -e "s|BUILDLDPATH=|$BUILDLDPATH|" \
-+    -e "s|MANDIRDIRECTORY|$MANDIR|" \
-+    -e "s|DOCDIRDIRECTORY|$DOCDIR|" \
-+    -e "s|EMACSLIBDIRECTORY|$EMACSLIB|" \
-+    -e "s|EMACSCOMMAND|$EMACS|" \
-+    -e "s|COQDOCDIRECTORY|$COQDOCDIR|" \
-+    -e "s|MKTEXLSRCOMMAND|$MKTEXLSR|" \
-+    -e "s|ARCHITECTURE|$ARCH|" \
-+    -e "s|OSDEPENDENTLIBS|$OSDEPLIBS|" \
-+    -e "s|OSDEPENDENTP4OPTFLAGS|$OSDEPP4OPTFLAGS|" \
-+    -e "s|CAMLLIBDIRECTORY|$CAMLLIB|" \
-+    -e "s|CAMLTAG|$CAMLTAG|" \
-+    -e "s|CAMLP4BINDIRECTORY|$CAMLP4BIN|" \
-+    -e "s|CAMLP4LIBDIRECTORY|$CAMLP4LIB|" \
-+    -e "s|CAMLP4TOOL|$camlp4oexec|" \
-+    -e "s|CAMLP4COMPATFLAGS|$CAMLP4COMPAT|" \
-+    -e "s|LABLGTKINCLUDES|$LABLGTKINCLUDES|" \
-+    -e "s|COQDEBUGFLAGOPT|$coq_debug_flag_opt|" \
-+    -e "s|COQDEBUGFLAG|$coq_debug_flag|" \
-+    -e "s|COQPROFILEFLAG|$coq_profile_flag|" \
-+    -e "s|CAMLANNOTATEFLAG|$coq_annotate_flag|" \
-+    -e "s|CCOMPILEFLAGS|$cflags|" \
-+    -e "s|BESTCOMPILER|$best_compiler|" \
-+    -e "s|DLLEXTENSION|$DLLEXT|" \
-+    -e "s|EXECUTEEXTENSION|$EXE|" \
-+    -e "s|BYTECAMLC|$bytecamlc|" \
-+    -e "s|OCAMLMKLIBEXEC|$ocamlmklibexec|" \
-+    -e "s|NATIVECAMLC|$nativecamlc|" \
-+    -e "s|OCAMLEXEC|$ocamlexec|" \
-+    -e "s|OCAMLDEPEXEC|$ocamldepexec|" \
-+    -e "s|OCAMLDOCEXEC|$ocamldocexec|" \
-+    -e "s|OCAMLLEXEXEC|$ocamllexexec|" \
-+    -e "s|OCAMLYACCEXEC|$ocamlyaccexec|" \
-+    -e "s|CAMLMKTOPEXEC|$ocamlmktopexec|" \
-+    -e "s|CCEXEC|$gcc_exec|" \
-+    -e "s|AREXEC|$ar_exec|" \
-+    -e "s|RANLIBEXEC|$ranlib_exec|" \
-+    -e "s|STRIPCOMMAND|$STRIPCOMMAND|" \
-+    -e "s|COQIDEOPT|$COQIDE|" \
-+    -e "s|CHECKEDOUTSOURCETREE|$checkedout|" \
-+    -e "s|WITHDOCOPT|$with_doc|" \
-+    -e "s|HASNATIVEDYNLINK|$NATDYNLINKFLAG|" \
-+      "$config_template" > "$config_file"
-+
-+chmod a-w "$config_file"
-+
-+##################################################
-+# The end
-+####################################################
-+
-+echo "If anything in the above is wrong, please restart './configure'."
-+echo
-+echo "*Warning* To compile the system for a new architecture"
-+echo "          don't forget to do a 'make archclean' before './configure'."
-+
-+# $Id: configure 14833 2011-12-19 21:57:30Z notin $
diff --git a/pkgs/applications/science/logic/coq/no-codesign.patch b/pkgs/applications/science/logic/coq/no-codesign.patch
deleted file mode 100644
index 0f917fbf56d4..000000000000
--- a/pkgs/applications/science/logic/coq/no-codesign.patch
+++ /dev/null
@@ -1,19 +0,0 @@
-diff --git a/Makefile.build b/Makefile.build
-index 2963a3d..876479c 100644
---- a/Makefile.build
-+++ b/Makefile.build
-@@ -101,13 +101,8 @@ BYTEFLAGS=$(CAMLDEBUG) $(USERFLAGS)
- OPTFLAGS=$(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS)
- DEPFLAGS= $(LOCALINCLUDES) -I ide -I ide/utils
- 
--ifeq ($(ARCH),Darwin)
--LINKMETADATA=-ccopt "-sectcreate __TEXT __info_plist config/Info-$(notdir $@).plist"
--CODESIGN=codesign -s -
--else
- LINKMETADATA=
- CODESIGN=true
--endif
- 
- define bestocaml
- $(if $(OPT),\
-
diff --git a/pkgs/top-level/aliases.nix b/pkgs/top-level/aliases.nix
index f06044829b4d..1617f9330b49 100644
--- a/pkgs/top-level/aliases.nix
+++ b/pkgs/top-level/aliases.nix
@@ -329,7 +329,7 @@ mapAliases ({
   callPackage_i686 = pkgsi686Linux.callPackage;
 
   inherit (ocaml-ng) # added 2016-09-14
-    ocamlPackages_3_11_2 ocamlPackages_3_12_1
+    ocamlPackages_3_12_1
     ocamlPackages_4_00_1 ocamlPackages_4_01_0 ocamlPackages_4_02
     ocamlPackages_4_03
     ocamlPackages_latest;
@@ -348,7 +348,6 @@ mapAliases ({
     gst-ffmpeg = pkgs.gst-ffmpeg;
   };
 } // (with ocaml-ng; { # added 2016-09-14
-  ocaml_3_11_2 = ocamlPackages_3_11_2.ocaml;
   ocaml_3_12_1 = ocamlPackages_3_12_1.ocaml;
   ocaml_4_00_1 = ocamlPackages_4_00_1.ocaml;
   ocaml_4_01_0 = ocamlPackages_4_01_0.ocaml;
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 2ed05e4972f1..632b88c8012c 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -21148,12 +21148,11 @@ with pkgs;
   boogie = dotnetPackages.Boogie;
 
   inherit (callPackage ./coq-packages.nix {
-    inherit (ocaml-ng) ocamlPackages_3_12_1
-                       ocamlPackages_4_02
+    inherit (ocaml-ng) ocamlPackages_4_02
                        ocamlPackages_4_05
     ;
   }) mkCoqPackages
-    coq_8_3 coq_8_4 coq_8_5 coq_8_6 coq_8_7 coq_8_8
+    coq_8_4 coq_8_5 coq_8_6 coq_8_7 coq_8_8
     coqPackages_8_5 coqPackages_8_6 coqPackages_8_7 coqPackages_8_8
     coqPackages coq
   ;
@@ -21232,7 +21231,17 @@ with pkgs;
 
   ltl2ba = callPackage ../applications/science/logic/ltl2ba {};
 
-  inherit (ocaml-ng.ocamlPackages_3_11_2) matita;
+  #inherit (ocaml-ng.ocamlPackages_3_11_2) matita;
+
+  # Current version is 0.5.8. Official website says:
+
+  # Version 0.5.9, released on December 23, 2014, is an update of version 0.5.8
+  # to compile with the latter OCaml version and libraries.
+  # It is unsupported, but still used for teaching at the University of Bologna.
+
+  # It should allow us removing the dependency on OCaml 3.11 but I haven't been
+  # able to confirm because Matita depends on lablgtkmathview-0.7.2 which
+  # already reports as broken.
 
   matita_130312 = lowPrio ocamlPackages.matita_130312;
 
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index bc21137903af..305d9ba351ba 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -1,6 +1,5 @@
 { lib, callPackage, newScope, recurseIntoAttrs
 , gnumake3
-, ocamlPackages_3_12_1
 , ocamlPackages_4_02
 , ocamlPackages_4_05
 }:
@@ -56,12 +55,6 @@ in rec {
     let self = mkCoqPackages' self coq; in
     filterCoqPackages coq self;
 
-  coq_8_3 = callPackage ../applications/science/logic/coq/8.3.nix {
-    make = gnumake3;
-    inherit (ocamlPackages_3_12_1) ocaml findlib;
-    camlp5 = ocamlPackages_3_12_1.camlp5_transitional;
-    lablgtk = ocamlPackages_3_12_1.lablgtk_2_14;
-  };
   coq_8_4 = callPackage ../applications/science/logic/coq/8.4.nix {
     inherit (ocamlPackages_4_02) ocaml findlib lablgtk;
     camlp5 = ocamlPackages_4_02.camlp5_transitional;
diff --git a/pkgs/top-level/ocaml-packages.nix b/pkgs/top-level/ocaml-packages.nix
index 026bab235065..ee0f554efa3f 100644
--- a/pkgs/top-level/ocaml-packages.nix
+++ b/pkgs/top-level/ocaml-packages.nix
@@ -1065,8 +1065,6 @@ in rec
 
   inherit mkOcamlPackages;
 
-  ocamlPackages_3_11_2 = mkOcamlPackages (callPackage ../development/compilers/ocaml/3.11.2.nix { }) (self: super: { lablgtk = self.lablgtk_2_14; });
-
   ocamlPackages_3_12_1 = mkOcamlPackages (callPackage ../development/compilers/ocaml/3.12.1.nix { }) (self: super: { camlimages = self.camlimages_4_0; });
 
   ocamlPackages_4_00_1 = mkOcamlPackages (callPackage ../development/compilers/ocaml/4.00.1.nix { }) (self: super: { });