Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 199 insertions, 162 deletions

diff --git a/configure b/configure
index db7a55a0..fb6dac1e 100755
--- a/configure
+++ b/configure
@@ -6,9 +6,9 @@
 # 
 ##################################
 
-VERSION=8.2pl2
-VOMAGIC=08200
-STATEMAGIC=58200
+VERSION=8.3-bugfix
+VOMAGIC=08300
+STATEMAGIC=58300
 DATE=`LANG=C date +"%B %Y"`
 
 # Create the bin/ directory if non-existent
@@ -63,11 +63,12 @@ usage () {
     printf "\tSpecifies the architecture\n"
     echo "-opt"
     printf "\tSpecifies whether or not to use OCaml *.opt optimized compilers\n"
-    echo "-fsets (all|basic)"
-    echo "-reals (all|basic)"
-    printf "\tSpecifies whether or not to compile full FSets/Reals library\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 "-uim-script-path"
+    printf "\tSpecifies where uim's .scm files are installed\n"
     echo "-browser <command>"
     printf "\tUse <command> to open URL %%s\n"
     echo "-with-doc (yes|no)"
@@ -108,6 +109,7 @@ coq_profile_flag=
 coq_annotate_flag=
 best_compiler=opt
 cflags="-fno-defer-pop -Wall -Wno-unused"
+natdynlink=yes
 
 gcc_exec=gcc
 ar_exec=ar
@@ -128,8 +130,6 @@ emacs_spec=no
 camldir_spec=no
 lablgtkdir_spec=no
 coqdocdir_spec=no
-fsets=all
-reals=all
 arch_spec=no
 coqide_spec=no
 browser_spec=no
@@ -137,6 +137,8 @@ wwwcoq_spec=no
 with_geoproof=false
 with_doc=all
 with_doc_spec=no
+force_caml_version=no
+force_caml_version_spec=no
 
 COQSRC=`pwd`
 
@@ -198,16 +200,11 @@ while : ; do
     -opt|--opt) bytecamlc=ocamlc.opt
                 camlp4oexec=camlp4o  # can't add .opt since dyn load'll be required
                 nativecamlc=ocamlopt.opt;;
-    -fsets|--fsets) case "$2" in
-			yes|all) fsets=all;;
-			*) fsets=basic
-		    esac
-		    shift;;
-    -reals|--reals) case "$2" in
-			yes|all) reals=all;;
-			*) reals=basic
-		    esac
-		    shift;;
+    -natdynlink|--natdynlink) case "$2" in
+	                  yes) natdynlink=yes;;
+                          *) natdynlink=no
+                        esac
+                        shift;;
     -coqide|--coqide) coqide_spec=yes
 		      case "$2" in
 			  byte|opt) COQIDE=$2;;
@@ -227,7 +224,7 @@ while : ; do
 		      esac
 		      shift;;
     -with-geoproof|--with-geoproof) 
-	  case $2 in
+	  case "$2" in
 	      yes) with_geoproof=true;;
 	      no) with_geoproof=false;;
 	  esac
@@ -248,13 +245,19 @@ while : ; do
     -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;;
+    -uim-script-path)
+          uim_script_path=$2
+          shift;;
     *) 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 "Options -prefix and -local are incompatible."
   echo "Configure script failed!"
   exit 1
 fi
@@ -288,7 +291,7 @@ case $arch_spec in
  	elif test -x /usr/bin/uname ; then
  	    ARCH=`/usr/bin/uname -s`
 	else
-	    echo "I can not automatically find the name of your architecture"
+	    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
@@ -334,7 +337,7 @@ if [ "$MAKE" != "" ]; then
 	  if [ "$MAKEVERSION" = "GNU Make 3.81" ]; then OK="yes"; fi
       fi
       if [ $OK = "no" ]; then
-	  echo "GNU Make >= 3.81 is needed"
+	  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"
@@ -343,14 +346,14 @@ if [ "$MAKE" != "" ]; then
           echo "  make"
           echo "  mv make .."
 	  echo "  cd .."
-	  echo "Restart then the configure script and later use ./make instead of make"
+	  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
   esac
 else
-  echo "Cannot find GNU Make 3.81"
+  echo "Cannot find GNU Make 3.81."
 fi
 
 # Browser command
@@ -400,7 +403,7 @@ case $camldir_spec in
 esac
 
 if test ! -f "$CAMLC" ; then
-    echo "I can not find the executable '$CAMLC'! (Have you installed it?)"
+    echo "I can not find the executable '$CAMLC'. Have you installed it?"
     echo "Configuration script failed!"
     exit 1
 fi
@@ -410,24 +413,18 @@ case $ARCH in
     win32) CAMLBIN=`cygpath -m ${CAMLBIN}`;;
 esac
 
-# this fixes a camlp4 bug under FreeBSD
-# ("native-code program cannot do a dynamic load")
-if [ `uname -s` = "FreeBSD" ]; then camlp4oexec=$camlp4oexec.byte; fi
-
 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.08.0)
+    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.[012])
 	echo "Your version of Objective-Caml is $CAMLVERSION."
-	if [ "$CAMLVERSION" = "3.08.0" ] ; then
-	    echo "You need Objective-Caml 3.07 or later (to the exception of 3.08.0)!"
+	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.07 or later!"
-	fi
-	echo "Configuration script failed!"
-	exit 1;;
-    3.07*|3.08*)
-	echo "You have Objective-Caml $CAMLVERSION. Good!";;
+	    echo "          You need Objective-Caml 3.09.3 or later."
+	    echo "          Configuration script failed!"
+	    exit 1
+	fi;;
     ?*)
 	CAMLP4COMPAT="-loc loc" 
 	echo "You have Objective-Caml $CAMLVERSION. Good!";;
@@ -449,7 +446,7 @@ case $ARCH in
       CAMLLIB=`"$CAMLC" -where`
 esac
 
-# We need to set va special flag for OCaml 3.07
+# We need to set a special flag for OCaml 3.07
 case  $CAMLVERSION in 
 	3.07*)
 	  cflags="$cflags -DOCAML_307";;
@@ -465,19 +462,42 @@ if [ "$coq_debug_flag" = "-g" ]; then
 fi
 
 # Native dynlink
-if test -f `"$CAMLC" -where`/dynlink.cmxa; then
+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 "Cannot find camlp5 libraries in $camlp5dir (camlp5.cma not found)."
 	echo "Configuration script failed!"
 	exit 1
     fi
@@ -632,11 +652,14 @@ case $COQIDE in
     no) LABLGTKINCLUDES="";;
 esac
 
-# Tell on windows if ocaml understands cygwin or windows path formats
-
-#"$CAMLC" -o config/giveostype config/giveostype.ml
-#CAMLOSTYPE=`config/giveostype`
-#rm config/giveostype
+if which uim-fep; then
+    for cand in i"$uim_script_path" /usr/local/share/uim/ /usr/share/uim/; do
+        if [ -f "$cand/loader.scm" ]; then
+            UIMSCRIPTDIR=$cand
+            break
+        fi
+    done
+fi
 
 # strip command
 
@@ -747,13 +770,13 @@ case $mandir_spec/$prefix_spec/$local in
 esac
 
 case $docdir_spec/$prefix_spec/$local in
-    yes/*/*) DOCDIR=$docdir;;
-    */yes/*) DOCDIR=$prefix/share/doc/coq ;;
-    */*/true) DOCDIR=$COQTOP/man ;;
+    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;;
+	    "") DOCDIR=$docdir_def; HTMLREFMANDIR=$DOCDIR/html/refman;;
 	    *) true;;
 	esac;;
 esac
@@ -822,6 +845,8 @@ esac
 #     yes) EMACS=$emacs;;
 # esac
 
+
+
 ###########################################
 # Summary of the configuration
 
@@ -838,19 +863,12 @@ 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 "$fsets" = "all"; then
-echo "  FSets theory                      : All"
-else
-echo "  FSets theory                      : Basic"
-fi
-if test "$reals" = "all"; then
-echo "  Reals theory                      : All"
-else
-echo "  Reals theory                      : Basic"
-fi
 if test "$with_doc" = "all"; then
 echo "  Documentation                     : All"
 else
@@ -869,9 +887,51 @@ echo "    documentation will be copied in $DOCDIR"
 echo "    emacs mode    will be copied in $EMACSLIB"
 echo ""
 
-#####################################################
-# Building the $COQTOP/config/coq_config.ml file
-#####################################################
+##################################################
+# 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 () {
@@ -882,64 +942,73 @@ EOF
 
 # Escaped version of browser command
 export BROWSER
-ESCBROWSER=`VAR=BROWSER escape_var`
+BROWSER=`VAR=BROWSER escape_var`
 
 # damned backslashes under M$Windows
 case $ARCH in
     win32)
-	ESCCOQTOP=`echo $COQTOP |sed -e 's|\\\|\\\\\\\|g'`
-	ESCBINDIR=`echo $BINDIR |sed -e 's|\\\|\\\\\\\|g'`
-	ESCSRCDIR=`cygpath -m $COQSRC |sed -e 's|\\\|\\\\\\\|g'`
-	ESCLIBDIR=`echo $LIBDIR |sed -e 's|\\\|\\\\\\\|g'`
-	ESCCAMLDIR=`echo $CAMLBIN |sed -e 's|\\\|\\\\\\\|g'`
-	ESCCAMLLIB=`echo $CAMLLIB |sed -e 's|\\\|\\\\\\\|g'`
-  	ESCMANDIR=`echo $MANDIR |sed -e 's|\\\|\\\\\\\|g'`
-  	ESCDOCDIR=`echo $DOCDIR |sed -e 's|\\\|\\\\\\\|g'`
-   	ESCEMACSLIB=`echo $EMACSLIB |sed -e 's|\\\|\\\\\\\|g'`
-   	ESCCOQDOCDIR=`echo $COQDOCDIR |sed -e 's|\\\|\\\\\\\|g'`
-   	ESCCAMLP4BIN=`echo $CAMLP4BIN |sed -e 's|\\\|\\\\\\\|g'`
-	ESCCAMLP4LIB=`echo $CAMLP4LIB |sed -e 's|\\\|\\\\\\\|g'`
-	ESCLABLGTKINCLUDES=`echo $LABLGTKINCLUDES |sed -e 's|\\\|\\\\\\\|g'`
-	ESCCOQRUNBYTEFLAGS=`echo $COQRUNBYTEFLAGS |sed -e 's|\\\|\\\\\\\|g'`
-	ESCCOQTOOLSBYTEFLAGS=`echo $COQTOOLSBYTEFLAGS |sed -e 's|\\\|\\\\\\\|g'`
-	ESCBUILDLDPATH=`echo $BUILDLDPATH |sed -e 's|\\\|\\\\\\\|g'`
-;;
-    *)
-        ESCCOQTOP="$COQTOP"
-	ESCBINDIR="$BINDIR"
-	ESCSRCDIR="$COQSRC"
-	ESCLIBDIR="$LIBDIR"
-	ESCCAMLDIR="$CAMLBIN"
-	ESCCAMLLIB="$CAMLLIB"
-  	ESCMANDIR="$MANDIR"
-  	ESCDOCDIR="$DOCDIR"
-   	ESCEMACSLIB="$EMACSLIB"
-   	ESCCOQDOCDIR="$COQDOCDIR"
-   	ESCCAMLP4BIN="$CAMLP4BIN"
-   	ESCCAMLP4LIB="$CAMLP4LIB"
-	ESCLABLGTKINCLUDES="$LABLGTKINCLUDES"
-	ESCCOQRUNBYTEFLAGS="$COQRUNBYTEFLAGS"
-	ESCCOQTOOLSBYTEFLAGS="$COQTOOLSBYTEFLAGS"
-	;;
+	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
 
-mlconfig_file="$COQSRC/config/coq_config.ml"
+#####################################################
+# 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 = "$ESCCOQRUNBYTEFLAGS"
-let coqlib = "$ESCLIBDIR"
-let coqsrc = "$ESCSRCDIR"
-let camlbin = "$ESCCAMLDIR"
-let camllib = "$ESCCAMLLIB"
+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 camlp4bin = "$ESCCAMLP4BIN"
-let camlp4lib = "$ESCCAMLP4LIB"
+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"
@@ -949,10 +1018,11 @@ let vo_magic_number = $VOMAGIC
 let state_magic_number = $STATEMAGIC
 let exec_extension = "$EXE"
 let with_geoproof = ref $with_geoproof
-let browser = "$ESCBROWSER"
+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
 
@@ -961,15 +1031,15 @@ 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" {} \; \) | grep -v correctness >> "$mlconfig_file")
+    (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 contrib_dirs = [" >> "$mlconfig_file"
-subdirs contrib
+echo "let plugins_dirs = [" >> "$mlconfig_file"
+subdirs plugins
 echo "]" >> "$mlconfig_file"
 
 chmod a-w "$mlconfig_file"
@@ -979,32 +1049,32 @@ chmod a-w "$mlconfig_file"
 # Building the $COQTOP/config/Makefile file
 ###############################################
 
-rm -f "$COQSRC/config/Makefile"
+rm -f "$config_file"
 
 sed -e "s|LOCALINSTALLATION|$local|" \
-    -e "s|XCOQRUNBYTEFLAGS|$ESCCOQRUNBYTEFLAGS|" \
-    -e "s|XCOQTOOLSBYTEFLAGS|$ESCCOQTOOLSBYTEFLAGS|" \
+    -e "s|XCOQRUNBYTEFLAGS|$COQRUNBYTEFLAGS|" \
+    -e "s|XCOQTOOLSBYTEFLAGS|$COQTOOLSBYTEFLAGS|" \
     -e "s|COQSRCDIRECTORY|$COQSRC|" \
     -e "s|COQVERSION|$VERSION|" \
-    -e "s|BINDIRDIRECTORY|$ESCBINDIR|" \
-    -e "s|COQLIBDIRECTORY|$ESCLIBDIR|" \
-    -e "s|BUILDLDPATH=|$ESCBUILDLDPATH|" \
-    -e "s|MANDIRDIRECTORY|$ESCMANDIR|" \
-    -e "s|DOCDIRDIRECTORY|$ESCDOCDIR|" \
-    -e "s|EMACSLIBDIRECTORY|$ESCEMACSLIB|" \
+    -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|$ESCCOQDOCDIR|" \
+    -e "s|COQDOCDIRECTORY|$COQDOCDIR|" \
     -e "s|MKTEXLSRCOMMAND|$MKTEXLSR|" \
     -e "s|ARCHITECTURE|$ARCH|" \
     -e "s|OSDEPENDENTLIBS|$OSDEPLIBS|" \
     -e "s|OSDEPENDENTP4OPTFLAGS|$OSDEPP4OPTFLAGS|" \
-    -e "s|CAMLLIBDIRECTORY|$ESCCAMLLIB|" \
+    -e "s|CAMLLIBDIRECTORY|$CAMLLIB|" \
     -e "s|CAMLTAG|$CAMLTAG|" \
-    -e "s|CAMLP4BINDIRECTORY|$ESCCAMLP4BIN|" \
+    -e "s|CAMLP4BINDIRECTORY|$CAMLP4BIN|" \
     -e "s|CAMLP4LIBDIRECTORY|$CAMLP4LIB|" \
     -e "s|CAMLP4TOOL|$camlp4oexec|" \
     -e "s|CAMLP4COMPATFLAGS|$CAMLP4COMPAT|" \
-    -e "s|LABLGTKINCLUDES|$ESCLABLGTKINCLUDES|" \
+    -e "s|LABLGTKINCLUDES|$LABLGTKINCLUDES|" \
     -e "s|COQDEBUGFLAGOPT|$coq_debug_flag_opt|" \
     -e "s|COQDEBUGFLAG|$coq_debug_flag|" \
     -e "s|COQPROFILEFLAG|$coq_profile_flag|" \
@@ -1026,55 +1096,22 @@ sed -e "s|LOCALINSTALLATION|$local|" \
     -e "s|AREXEC|$ar_exec|" \
     -e "s|RANLIBEXEC|$ranlib_exec|" \
     -e "s|STRIPCOMMAND|$STRIPCOMMAND|" \
-    -e "s|FSETSOPT|$fsets|" \
-    -e "s|REALSOPT|$reals|" \
     -e "s|COQIDEOPT|$COQIDE|" \
     -e "s|CHECKEDOUTSOURCETREE|$checkedout|" \
     -e "s|WITHDOCOPT|$with_doc|" \
-    -e "s|HASNATIVEDYNLINK|$HASNATDYNLINK|" \
-      "$COQSRC/config/Makefile.template" > "$COQSRC/config/Makefile"
-
-chmod a-w "$COQSRC/config/Makefile"
-
-##################################################
-# 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) 
-####################################################
+    -e "s|HASNATIVEDYNLINK|$NATDYNLINKFLAG|" \
+    -e "s|UIMSCRIPTPATH|$UIMSCRIPTDIR|" \
+      "$config_template" > "$config_file"
 
-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  
+chmod a-w "$config_file"
 
 ##################################################
 # The end
 ####################################################
 
-echo "If anything in the above is wrong, please restart './configure'"
+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 13223 2010-06-29 18:28:35Z notin $
+# $Id: configure 12689 2010-01-26 13:41:56Z glondu $