Imported Upstream version 8.4~betaupstream/8.4_beta

1 files changed, 207 insertions, 90 deletions

diff --git a/configure b/configure
index 8498bd70..867ee935 100755
--- a/configure
+++ b/configure
@@ -6,10 +6,10 @@
 # 
 ##################################
 
-VERSION=8.3pl3
-VOMAGIC=08300
-STATEMAGIC=58300
-DATE=`LANG=C date +"%B %Y"`
+VERSION=8.4beta
+VOMAGIC=08400
+STATEMAGIC=58400
+DATE="December 2011"
 
 # Create the bin/ directory if non-existent
 test -d bin || mkdir bin
@@ -45,9 +45,11 @@ usage () {
     printf "\tSpecifies the source directory\n"
     echo "-bindir"
     echo "-libdir"
+    echo "-configdir"
+    echo "-datadir"
     echo "-mandir"
     echo "-docdir"
-    printf "\tSpecifies where to install bin/lib/man/doc files resp.\n"
+    printf "\tSpecifies where to install bin/lib/config/data/man/doc files resp.\n"
     echo "-emacslib"
     echo "-emacs"
     printf "\tSpecifies where emacs files are to be installed\n"
@@ -57,6 +59,10 @@ usage () {
     printf "\tSpecifies the path to the OCaml library\n"
     echo "-lablgtkdir"
     printf "\tSpecifies the path to the Lablgtk library\n"
+    echo "-usecamlp5"
+    printf "\tSpecifies to use camlp5 instead of camlp4\n"
+    echo "-usecamlp4"
+    printf "\tSpecifies to use camlp4 instead of camlp5\n"
     echo "-camlp5dir"
     printf "\tSpecifies where to look for the Camlp5 library and tells to use it\n"
     echo "-arch"
@@ -67,6 +73,8 @@ usage () {
     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 "-nomacintegration"
+    printf "\tSpecifies to not try to build coqide mac integration\n"
     echo "-browser <command>"
     printf "\tUse <command> to open URL %%s\n"
     echo "-with-doc (yes|no)"
@@ -85,6 +93,8 @@ usage () {
     printf "\tAdd profiling information in the Coq executables\n"
     echo "-annotate"
     printf "\tCompiles Coq with -dtypes option\n"
+    echo "-makecmd <command>"
+    printf "\tName of GNU Make command.\n"
 }
 
 
@@ -121,6 +131,8 @@ src_spec=no
 prefix_spec=no
 bindir_spec=no
 libdir_spec=no
+configdir_spec=no
+datadir_spec=no
 mandir_spec=no
 docdir_spec=no
 emacslib_spec=no
@@ -130,6 +142,7 @@ lablgtkdir_spec=no
 coqdocdir_spec=no
 arch_spec=no
 coqide_spec=no
+nomacintegration_spec=no
 browser_spec=no
 wwwcoq_spec=no
 with_geoproof=false
@@ -137,6 +150,7 @@ with_doc=all
 with_doc_spec=no
 force_caml_version=no
 force_caml_version_spec=no
+usecamlp5=yes
 
 COQSRC=`pwd`
 
@@ -168,6 +182,12 @@ while : ; do
     -libdir|--libdir) libdir_spec=yes
                       libdir="$2"
 		      shift;;
+    -configdir|--configdir) configdir_spec=yes
+                      configdir="$2"
+		      shift;;
+    -datadir|--datadir) datadir_spec=yes
+                      datadir="$2"
+		      shift;;
     -mandir|--mandir) mandir_spec=yes
                       mandir="$2"
 		      shift;;
@@ -189,7 +209,12 @@ while : ; do
     -lablgtkdir|--lablgtkdir) lablgtkdir_spec=yes
 	                lablgtkdir="$2"
 			shift;;
+    -usecamlp5|--usecamlp5)
+	                usecamlp5=yes;;
+    -usecamlp4|--usecamlp4)
+	                usecamlp5=no;;
     -camlp5dir|--camlp5dir)
+                        usecamlp5=yes
 	                camlp5dir="$2"
 			shift;;
     -arch|--arch) arch_spec=yes
@@ -209,6 +234,8 @@ while : ; do
 			  *) COQIDE=no
 		      esac
 		      shift;;
+    -nomacintegration) nomacintegration_spec=yes
+		      shift;;
     -browser|--browser) browser_spec=yes
 		      BROWSER=$2
 		      shift;;
@@ -239,6 +266,8 @@ while : ; do
 	  ranlib_spec=yes
 	  ranlib_exec=$2
 	  shift;;
+    -makecmd|--makecmd) makecmd="$2"
+		      shift;;
     -byte-only|-byteonly|--byteonly|--byte-only) best_compiler=byte;;
     -debug|--debug) coq_debug_flag=-g;;
     -profile|--profile) coq_profile_flag=-p;;
@@ -273,18 +302,19 @@ case $arch_spec in
     # First we test if we are running a Cygwin system
     if [ `uname -s | cut -c -6` = "CYGWIN" ] ; then
 	ARCH="win32"
+	CYGWIN=yes
     else
 	# If not, we determine the architecture
-	if test -x /bin/arch ; then
+	if test -x /bin/uname ; then
+ 	    ARCH=`/bin/uname -s`
+ 	elif test -x /usr/bin/uname ; then
+ 	    ARCH=`/usr/bin/uname -s`
+ 	elif 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"\
@@ -319,7 +349,7 @@ fi
 
 # make command
 
-MAKE=`which make`
+MAKE=`which ${makecmd:-make}`
 if [ "$MAKE" != "" ]; then
   MAKEVERSION=`$MAKE -v | head -1 | cut -d" " -f3`
   MAKEVERSIONMAJOR=`echo $MAKEVERSION | cut -d. -f1`
@@ -328,6 +358,8 @@ if [ "$MAKE" != "" ]; then
       echo "You have GNU Make $MAKEVERSION. Good!"
   else
       OK="no"
+      #Extra support for local installation of make 3.81
+      #will be useless when make >= 3.81 will be standard
       if [ -x ./make ]; then
 	  MAKEVERSION=`./make -v | head -1`
 	  if [ "$MAKEVERSION" = "GNU Make 3.81" ]; then OK="yes"; fi
@@ -357,6 +389,7 @@ fi
 if [ "$browser_spec" = "no" ]; then
     case $ARCH in
         win32) BROWSER='C:\PROGRA~1\INTERN~1\IEXPLORE %s' ;;
+	Darwin) BROWSER='open %s' ;;
         *) BROWSER='firefox -remote "OpenURL(%s,new-tab)" || firefox %s &' ;;
     esac
 fi
@@ -412,16 +445,16 @@ 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*)
+    1.*|2.*|3.0*)
 	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 "          You need Objective-Caml 3.10.0 or later."
 	    echo "          Configuration script failed!"
 	    exit 1
 	fi;;
-    ?*)
+    3.1*)
 	CAMLP4COMPAT="-loc loc" 
 	echo "You have Objective-Caml $CAMLVERSION. Good!";;
     *)
@@ -458,7 +491,7 @@ else
     HASNATDYNLINK=false
 fi
 
-case $HASNATDYNLINK,`uname -s`,`uname -r`,$CAMLVERSION in
+case $HASNATDYNLINK,$ARCH,`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
@@ -483,75 +516,76 @@ esac
 
 # Camlp4 / Camlp5 configuration
 
-if [ "$camlp5dir" != "" ]; then
+# Assume that camlp(4|5) binaries are at the same place as ocaml ones
+# (this should become configurable some day)
+CAMLP4BIN=${CAMLBIN}
+
+if [ "$usecamlp5" = "yes" ]; then
     CAMLP4=camlp5
-    CAMLP4LIB=$camlp5dir
-    if [ ! -f $camlp5dir/camlp5.cma ]; then
-	echo "Cannot find camlp5 libraries in $camlp5dir (camlp5.cma not found)."
+    CAMLP4MOD=gramlib
+    if [ "$camlp5dir" != "" ]; then
+	if [ -f "$camlp5dir/${CAMLP4MOD}.cma" ]; then
+	    CAMLP4LIB=$camlp5dir
+	    FULLCAMLP4LIB=$camlp5dir
+	else
+	    echo "Cannot find camlp5 libraries in $camlp5dir (camlp5.cma not found)."
+	    echo "Configuration script failed!"
+	    exit 1
+	fi
+    elif [ -f "${CAMLLIB}/camlp5/${CAMLP4MOD}.cma" ]; then
+        CAMLP4LIB=+camlp5
+	FULLCAMLP4LIB=${CAMLLIB}/camlp5
+    elif [ -f "${CAMLLIB}/site-lib/${CAMLP4MOD}.cma" ]; then
+        CAMLP4LIB=+site-lib/camlp5
+	FULLCAMLP4LIB=${CAMLLIB}/site-lib/camlp5
+    else
+	echo "Objective Caml $CAMLVERSION found but no Camlp5 installed."
 	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
-            ;;
+    case `$camlp4oexec -v 2>&1` in
+	*4.0*|*5.00*)
+	    echo "Camlp5 version < 5.01 not supported."
+	    echo "Configuration script failed!"
+	    exit 1;;
     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
+else # let's use camlp4
+    CAMLP4=camlp4
+    CAMLP4MOD=camlp4lib
+    CAMLP4LIB=+camlp4
+    FULLCAMLP4LIB=${CAMLLIB}/camlp4
 
+    if [ ! -f "${FULLCAMLP4LIB}/${CAMLP4MOD}.cma" ]; then
+	echo "Objective Caml $CAMLVERSION found but no Camlp4 installed."
+	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}
+    camlp4oexec=${camlp4oexec}rf
+    if [ "`$camlp4oexec 2>&1`" != "" ]; then
+	echo "Error: $camlp4oexec not found or not executable."
+	echo "Configuration script failed!"
+	exit 1
+    fi
+fi
 
 # 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
+      if [ ! -f "${FULLCAMLP4LIB}/${CAMLP4MOD}.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!"
+          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
@@ -569,7 +603,6 @@ case $ARCH in
 	   *) OS="Sun OS $OS"
 	      OSDEPLIBS="-cclib -lunix"
         esac;;
-  alpha) OSDEPLIBS="-cclib -lunix";;
   win32) OS="Win32" 
 	 OSDEPLIBS="-cclib -lunix"
 	 cflags="-mno-cygwin $cflags";;
@@ -578,6 +611,10 @@ esac
 
 # lablgtk2 and CoqIDE
 
+IDEARCHFLAGS=
+IDEARCHFILE=
+IDEARCHDEF=X11
+
 # -byte-only should imply -coqide byte, unless the user decides otherwise
 
 if [ "$best_compiler" = "byte" -a "$coqide_spec" = "no" ]; then 
@@ -616,9 +653,21 @@ else
     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."
+    else
+        echo "LablGtk2 found, native threads: native CoqIde will be available."
 	COQIDE=opt
+        if [ "$nomacintegration_spec" = "no" ] && pkg-config --exists ige-mac-integration;
+        then
+            cflags=$cflags" `pkg-config --cflags ige-mac-integration`"
+	    IDEARCHFLAGS='-ccopt "`pkg-config --libs ige-mac-integration`"'
+	    IDEARCHFILE=ide/ide_mac_stubs.o
+	    IDEARCHDEF=QUARTZ
+	elif [ "$ARCH" = "win32" ];
+        then
+	    IDEARCHFLAGS=
+	    IDEARCHFILE=ide/ide_win32_stubs.o
+	    IDEARCHDEF=WIN32
+	fi
     fi
 fi
 
@@ -627,8 +676,8 @@ case $COQIDE in
         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
+            yes) LABLGTKLIB=$lablgtkdir               # Pour le message
+                 LABLGTKINCLUDES="-I $LABLGTKLIB";; # Pour le makefile
         esac;;
     no) LABLGTKINCLUDES="";;
 esac
@@ -639,9 +688,14 @@ case $ARCH in
     win32)
 	# true -> strip : it exists under cygwin !
 	STRIPCOMMAND="strip";; 
+    Darwin) if [ "$HASNATDYNLINK" = "true" ]
+	then
+	  STRIPCOMMAND="true"
+	else
+	  STRIPCOMMAND="strip"
+	fi;;
     *)
-    if [ "$coq_profile_flag" = "-p" ] || [ "$coq_debug_flag" = "-g" ] ||
-       [ "`uname -s`" = "Darwin" -a "$HASNATDYNLINK" = "true" ]
+    if [ "$coq_profile_flag" = "-p" ] || [ "$coq_debug_flag" = "-g" ]
     then
 	STRIPCOMMAND="true"
     else
@@ -682,18 +736,23 @@ case $ARCH in
     win32) COQTOP=`cygpath -m ${COQTOP}`
 esac
 
-case $ARCH in
+case $ARCH$CYGWIN 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';;
+	 W32PREF='C:\\coq\\'
+	 bindir_def=${W32PREF}bin
+	 libdir_def=${W32PREF}lib
+	 configdir_def=${W32PREF}config
+	 datadir_def=${W32PREF}data
+	 mandir_def=${W32PREF}man
+	 docdir_def=${W32PREF}doc
+	 emacslib_def=${W32PREF}emacs
+         coqdocdir_def=${W32PREF}latex;;
   *)
 	 bindir_def=/usr/local/bin
 	 libdir_def=/usr/local/lib/coq
-	 mandir_def=/usr/local/man
+	 configdir_def=/etc/xdg/coq
+	 datadir_def=/usr/local/share/coq
+	 mandir_def=/usr/local/share/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;;
@@ -716,6 +775,7 @@ esac
 case $libdir_spec/$prefix_spec/$local in
     yes/*/*) LIBDIR=$libdir;;
     */yes/*)
+        libdir_spec=yes
         case $ARCH in
           win32) LIBDIR=$prefix ;;
           *)  LIBDIR=$prefix/lib/coq ;;
@@ -723,15 +783,57 @@ case $libdir_spec/$prefix_spec/$local in
     */*/true) LIBDIR=$COQTOP ;;
     *)  printf "Where should I install the Coq library [$libdir_def]? "
         read LIBDIR
+        libdir_spec=yes
 	case $LIBDIR in
 	    "") LIBDIR=$libdir_def;;
 	    *) true;;
 	esac;;
 esac
 
+case $libdir_spec in
+    yes) LIBDIR_OPTION="Some \"$LIBDIR\"";;
+    *) LIBDIR_OPTION="None";;
+esac
+
+case $configdir_spec/$local in
+    yes/*) CONFIGDIR=$configdir;;
+    */true) CONFIGDIR=$COQTOP/ide
+        configdir_spec=yes;;
+    *)  printf "Where should I install the Coqide configuration files [$configdir_def]? "
+        read CONFIGDIR
+	case $CONFIGDIR in
+	    "") CONFIGDIR=$configdir_def;;
+	    *) configdir_spec=yes;;
+	esac;;
+esac
+
+case $configdir_spec in
+    yes) CONFIGDIR_OPTION="Some \"$CONFIGDIR\"";;
+    *) CONFIGDIR_OPTION="None";;
+esac
+
+case $datadir_spec/$prefix_spec/$local in
+    yes/*/*) DATADIR=$datadir;;
+    */yes/*) DATADIR=$prefix/share/coq;;
+    */*/true) DATADIR=$COQTOP/ide
+        datadir_spec=yes;;
+    *)  printf "Where should I install the Coqide data files [$datadir_def]? "
+        read DATADIR
+	case $DATADIR in
+	    "") DATADIR=$datadir_def;;
+	    *) datadir_spec=yes;;
+	esac;;
+esac
+
+case $datadir_spec in
+    yes) DATADIR_OPTION="Some \"$DATADIR\"";;
+    *) DATADIR_OPTION="None";;
+esac
+
+
 case $mandir_spec/$prefix_spec/$local in
     yes/*/*) MANDIR=$mandir;;
-    */yes/*) MANDIR=$prefix/man ;;
+    */yes/*) MANDIR=$prefix/share/man ;;
     */*/true) MANDIR=$COQTOP/man ;;
     *)  printf "Where should I install the Coq man pages [$mandir_def]? "
         read MANDIR
@@ -742,13 +844,13 @@ case $mandir_spec/$prefix_spec/$local in
 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;;
+    yes/*/*) DOCDIR=$docdir;;
+    */yes/*) DOCDIR=$prefix/share/doc/coq;;
+    */*/true) DOCDIR=$COQTOP/doc;;
     *)  printf "Where should I install the Coq documentation [$docdir_def]? "
         read DOCDIR
 	case $DOCDIR in
-	    "") DOCDIR=$docdir_def; HTMLREFMANDIR=$DOCDIR/html/refman;;
+	    "") DOCDIR=$docdir_def;;
 	    *) true;;
 	esac;;
 esac
@@ -787,7 +889,7 @@ esac
 
 # Determine if we enable -custom by default (Windows and MacOS)
 CUSTOM_OS=no
-if [ "$ARCH" = "win32" ] || [ "`uname -s`" = "Darwin" ]; then
+if [ "$ARCH" = "win32" ] || [ "$ARCH" = "Darwin" ]; then
     CUSTOM_OS=yes
 fi
 
@@ -841,6 +943,9 @@ fi
 if test "$COQIDE" != "no"; then
 echo "  Lablgtk2 library in               : $LABLGTKLIB"
 fi
+if test "$IDEARCHDEF" = "QUARTZ"; then
+echo "  Mac OS integration is on"
+fi
 if test "$with_doc" = "all"; then
 echo "  Documentation                     : All"
 else
@@ -854,6 +959,8 @@ echo ""
 echo "  Paths for true installation:"
 echo "    binaries      will be copied in $BINDIR"
 echo "    library       will be copied in $LIBDIR"
+echo "    config files  will be copied in $CONFIGDIR"
+echo "    data files    will be copied in $DATADIR"
 echo "    man pages     will be copied in $MANDIR"
 echo "    documentation will be copied in $DOCDIR"
 echo "    emacs mode    will be copied in $EMACSLIB"
@@ -923,6 +1030,8 @@ case $ARCH in
 	BINDIR=`echo $BINDIR |sed -e 's|\\\|\\\\\\\|g'`
 	COQSRC=`cygpath -m $COQSRC |sed -e 's|\\\|\\\\\\\|g'`
 	LIBDIR=`echo $LIBDIR |sed -e 's|\\\|\\\\\\\|g'`
+	CONFIGDIR=`echo $CONFIGDIR |sed -e 's|\\\|\\\\\\\|g'`
+	DATADIR=`echo $DATADIR |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'`
@@ -957,8 +1066,10 @@ cat << END_OF_COQ_CONFIG > $mlconfig_file
 
 let local = $local
 let coqrunbyteflags = "$COQRUNBYTEFLAGS"
-let coqlib = "$LIBDIR"
-let coqsrc = "$COQSRC"
+let coqlib = $LIBDIR_OPTION
+let configdir = $CONFIGDIR_OPTION
+let datadir = $DATADIR_OPTION
+let docdir = "$DOCDIR"
 let ocaml = "$ocamlexec"
 let ocamlc = "$bytecamlc"
 let ocamlopt = "$nativecamlc"
@@ -979,6 +1090,7 @@ let cflags = "$cflags"
 let best = "$best_compiler"
 let arch = "$ARCH"
 let has_coqide = "$COQIDE"
+let gtk_platform = \`$IDEARCHDEF
 let has_natdynlink = $HASNATDYNLINK
 let natdynlinkflag = "$NATDYNLINKFLAG"
 let osdeplibs = "$OSDEPLIBS"
@@ -994,7 +1106,7 @@ let browser = "$BROWSER"
 let wwwcoq = "$WWWCOQ"
 let wwwrefman = wwwcoq ^ "distrib/" ^ version ^ "/refman/"
 let wwwstdlib = wwwcoq ^ "distrib/" ^ version ^ "/stdlib/"
-let localwwwrefman = "file://$HTMLREFMANDIR/"
+let localwwwrefman = "file:/" ^ docdir ^ "html/refman"
 
 END_OF_COQ_CONFIG
 
@@ -1030,6 +1142,8 @@ sed -e "s|LOCALINSTALLATION|$local|" \
     -e "s|COQVERSION|$VERSION|" \
     -e "s|BINDIRDIRECTORY|$BINDIR|" \
     -e "s|COQLIBDIRECTORY|$LIBDIR|" \
+    -e "s|CONFIGDIRDIRECTORY|$CONFIGDIR|" \
+    -e "s|DATADIRDIRECTORY|$DATADIR|" \
     -e "s|BUILDLDPATH=|$BUILDLDPATH|" \
     -e "s|MANDIRDIRECTORY|$MANDIR|" \
     -e "s|DOCDIRDIRECTORY|$DOCDIR|" \
@@ -1042,6 +1156,7 @@ sed -e "s|LOCALINSTALLATION|$local|" \
     -e "s|OSDEPENDENTP4OPTFLAGS|$OSDEPP4OPTFLAGS|" \
     -e "s|CAMLLIBDIRECTORY|$CAMLLIB|" \
     -e "s|CAMLTAG|$CAMLTAG|" \
+    -e "s|CAMLP4VARIANT|$CAMLP4|" \
     -e "s|CAMLP4BINDIRECTORY|$CAMLP4BIN|" \
     -e "s|CAMLP4LIBDIRECTORY|$CAMLP4LIB|" \
     -e "s|CAMLP4TOOL|$camlp4oexec|" \
@@ -1069,6 +1184,9 @@ sed -e "s|LOCALINSTALLATION|$local|" \
     -e "s|RANLIBEXEC|$ranlib_exec|" \
     -e "s|STRIPCOMMAND|$STRIPCOMMAND|" \
     -e "s|COQIDEOPT|$COQIDE|" \
+    -e "s|IDEARCHFLAGS|$IDEARCHFLAGS|" \
+    -e "s|IDEARCHFILE|$IDEARCHFILE|" \
+    -e "s|IDEARCHDEF|$IDEARCHDEF|" \
     -e "s|CHECKEDOUTSOURCETREE|$checkedout|" \
     -e "s|WITHDOCOPT|$with_doc|" \
     -e "s|HASNATIVEDYNLINK|$NATDYNLINKFLAG|" \
@@ -1085,4 +1203,3 @@ 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 $