Initial revision

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2 85f007b7-540e-0410-9357-904b9bb8a0f7

17 files changed, 1811 insertions, 0 deletions

diff --git a/.depend b/.depend
new file mode 100644
index 0000000000..c30d762a6f
--- /dev/null
+++ b/.depend
@@ -0,0 +1,15 @@
+kernel/names.cmi: lib/pp.cmi 
+lib/pp.cmi: lib/pp_control.cmi 
+lib/util.cmi: lib/pp.cmi 
+config/coq_config.cmo: config/coq_config.cmi 
+config/coq_config.cmx: config/coq_config.cmi 
+kernel/names.cmo: lib/hashcons.cmi lib/pp.cmi lib/util.cmi kernel/names.cmi 
+kernel/names.cmx: lib/hashcons.cmx lib/pp.cmx lib/util.cmx kernel/names.cmi 
+lib/hashcons.cmo: lib/hashcons.cmi 
+lib/hashcons.cmx: lib/hashcons.cmi 
+lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi 
+lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi 
+lib/pp_control.cmo: lib/pp_control.cmi 
+lib/pp_control.cmx: lib/pp_control.cmi 
+lib/util.cmo: lib/pp.cmi lib/util.cmi 
+lib/util.cmx: lib/pp.cmx lib/util.cmi 
diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000000..cb3d0b2a9f
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,68 @@
+
+# Main Makefile for Coq
+
+include config/Makefile
+
+noargument:
+	@echo Please use either
+	@echo "   ./configure"
+	@echo "   make world"
+	@echo "   make install"
+	@echo "   make cleanall"
+	@echo or make archclean
+
+INCLUDES=-I config -I lib
+BYTEFLAGS=$(INCLUDES) $(CAMLDEBUG)
+OPTFLAGS=$(INCLUDES) $(CAMLTIMEPROF)
+OCAMLDEP=ocamldep
+DEPFLAGS=$(INCLUDES)
+
+# Objects files 
+
+CONFIG=config/coq_config.cmo
+
+LIB=lib/pp_control.cmo lib/pp.cmo lib/util.cmo lib/hashcons.cmo
+
+KERNEL=kernel/names.cmo
+
+OBJS=$(CONFIG) $(LIB) $(KERNEL)
+
+# Targets
+
+world: $(OBJS)
+
+# Default rules
+
+.SUFFIXES: .ml .mli .cmo .cmi .cmx
+
+.ml.cmo:
+	$(OCAMLC) $(BYTEFLAGS) -c $<
+
+.mli.cmi:
+	$(OCAMLC) $(BYTEFLAGS) -c $<
+
+.ml.cmx:
+	$(OCAMLOPT) $(OPTFLAGS) -c $<
+
+# Cleaning
+
+archclean::
+	rm -f config/*.cmx config/*.[so]
+	rm -f lib/*.cmx lib/*.[so]
+	rm -f kernel/*.cmx kernel/*.[so]
+
+cleanall:: archclean
+	rm -f *~
+	rm -f config/*.cm[io] config/*~
+	rm -f lib/*.cm[io] lib/*~
+	rm -f kernel/*.cm[io] kernel/*~
+
+cleanconfig::
+	rm -f config/Makefile config/coq_config.ml
+
+# Dependencies
+
+depend:
+	$(OCAMLDEP) $(DEPFLAGS) */*.mli */*.ml > .depend
+
+include .depend
diff --git a/config/.cvsignore b/config/.cvsignore
new file mode 100644
index 0000000000..0fb99f4196
--- /dev/null
+++ b/config/.cvsignore
@@ -0,0 +1,2 @@
+Makefile
+coq_config.ml
diff --git a/config/Makefile.template b/config/Makefile.template
new file mode 100644
index 0000000000..8194bec773
--- /dev/null
+++ b/config/Makefile.template
@@ -0,0 +1,109 @@
+##################################
+#
+#  Configuration file for Coq
+# 
+##################################
+
+#############################################################################
+#
+#  This file is generated by the script "configure"
+#
+#  DO NOT EDIT IT !! DO NOT EDIT IT !! DO NOT EDIT IT !! DO NOT EDIT IT !! 
+#
+#  If something is wrong below, then rerun the script "configure"
+#  with the good options (see the file INSTALL).
+#
+#############################################################################
+
+# Paths for true installation
+# BINDIR=path where coqtop, coqc, coqmktop, coq-tex, coqdep, gallina and
+#        do_Makefile will reside
+# LIBDIR=path where the Coq library will reside
+# MANDIR=path where to install manual pages
+# EMACSDIR=path where to put Coq's Emacs mode (coq.el)
+BINDIR=BINDIRDIRECTORY
+COQLIB=COQLIBDIRECTORY
+MANDIR=MANDIRDIRECTORY
+EMACSLIB=EMACSLIBDIRECTORY
+EMACS=EMACSCOMMAND
+
+# Path to Coq distribution
+COQTOP=COQTOPDIRECTORY
+VERSION=COQVERSION
+
+# Path to the directory containing the objective-caml commands
+# Used in src/launch
+CAMLBIN=CAMLBINDIRECTORY
+
+# Directory containing Camlp4 binaries. Can be empty if camlp4 is in the PATH
+CAMLP4BIN=CAMLP4BINDIRECTORY
+
+# Camlp4 library directory
+CAMLP4LIB=CAMLP4LIBDIRECTORY
+
+# Objective-Caml compile command 
+OCAMLC=BYTECAMLC
+OCAMLOPT=NATIVECAMLC
+
+# Caml link command and Caml make top command
+CAMLLINK=BYTECAMLC
+CAMLOPTLINK=NATIVECAMLC
+CAMLMKTOP=ocamlmktop
+
+# Compilation debug flag
+CAMLDEBUG=COQDEBUGFLAG
+
+# Compilation profile flag
+CAMLTIMEPROF=COQPROFILEFLAG
+
+# Compilation of tools: bytecode (=byte) or native (=opt)
+COQTOOLS=COQTOOLSFLAG
+
+# For Camlp4 use
+P4=$(COQTOP)/bin/$(ARCH)/call_camlp4 -I $(COQTOP)/src/parsing
+P4DEP=$(COQTOP)/bin/$(ARCH)/camlp4dep
+
+# Your architecture
+# Can be obtain by UNIX command arch
+ARCH=ARCHITECTURE
+
+# Supplementary libs for some systems, currently:
+#  . Sun Solaris: -cclib -lunix -cclib -lnsl -cclib -lsocket
+#  . others     : -cclib -lunix
+#  . windows	: -cclib \\ocaml\lib\libunix.lib -cclib wsock32.lib
+
+OSDEPLIBS=OSDEPENDANTLIBS
+
+# Supplementary camlp4 flags for some systems, currently:
+#  . ppp        : -split_gext
+
+OSDEPP4OPTFLAGS=OSDEPENDANTP4OPTFLAGS
+
+# the caml str lib
+# Unix : -cclib -lstr
+# Windows : -cclib \\ocaml/lib/libstr.lib
+WITH_STR=STRLIBRARY
+
+# OStype is one of :
+# Unix
+# Win32
+OSTYPE=OSKIND
+
+# executable files extension, currently:
+#  Unix systems:
+#  Win32 systems : .exe
+EXE=EXECUTEEXTENSION
+
+# the command used to install binaries, libs and help files
+INSTALL=COQTOPDIRECTORY/bin/ARCHITECTURE/coqinstallEXECUTEEXTENSION
+
+# the command MKDIR (try to replace it with mkdirhier if you have problems)
+MKDIR=mkdir -p
+
+#the command STRIP 
+# Unix systems: strip
+# Win32 systems: true (actually strip is bogus)
+STRIP=STRIPCOMMAND
+
+# make or sed are bogus and believe lines not terminating by a return
+# are inexistent
\ No newline at end of file
diff --git a/config/coq_config.mli b/config/coq_config.mli
new file mode 100644
index 0000000000..83fcad46dd
--- /dev/null
+++ b/config/coq_config.mli
@@ -0,0 +1,24 @@
+
+(* $Id$ *)
+
+val bindir : string     (* where the binaries are installed *)
+val coqlib : string     (* where the std library is installed *)
+
+val coqtop : string     (* where are the sources *)
+
+val camllib : string    (* for Dynlink *)
+
+val camlp4lib : string  (* where is the library of Camlp4 *)
+
+val arch : string       (* architecture *)
+val osdeplibs : string  (* OS dependant link options for ocamlc *)
+
+val defined : string list  (* options for lib/ocamlpp *)
+
+val version : string    (* version number of Coq *)
+val versionsi : string  (* version number of Coq_SearchIsos *)
+val date : string       (* release date *)
+val compile_date : string (* compile date *)
+
+val theories_dirs : string list
+
diff --git a/configure b/configure
new file mode 100755
index 0000000000..b10fc6bad0
--- /dev/null
+++ b/configure
@@ -0,0 +1,474 @@
+#!/bin/sh
+
+##################################
+#
+#  Configuration script for Coq
+# 
+##################################
+
+VERSION=7.0
+VERSIONSI=1.0
+DATE="August 1999"
+
+# a local which command for sh
+which () {
+for i in `echo $PATH | tr ':' ' '` ; do 
+  if test -z "$i"; then $i=.; fi 
+  if [ -f $i/$1 ] ; then
+	echo $i/$1
+	break
+  fi
+done
+}
+
+bytecamlc=ocamlc
+nativecamlc=ocamlopt
+coq_debug_flag=
+coq_profile_flag=
+byte_opt_tools=opt
+
+bindir_spec=no
+libdir_spec=no
+mandir_spec=no
+emacslib_spec=no
+emacs_spec=no
+arch_spec=no
+caml_warnings=""
+
+COQTOP=`pwd`
+
+
+# Parse command-line arguments
+
+while : ; do
+  case "$1" in
+    "") break;;
+    -prefix|--prefix) bindir_spec=yes
+                      bindir=$2/bin
+                      libdir_spec=yes
+		      libdir=$2/lib/coq
+                      mandir_spec=yes
+		      mandir=$2/man
+		      shift;;
+    -local|--local) bindir_spec=yes
+                    bindir=$COQTOP/bin/${arch-`arch`}
+                    libdir_spec=yes
+		    libdir=$COQTOP
+                    mandir_spec=yes
+		    mandir=$COQTOP/man
+                    emacslib_spec=yes
+		    emacslib=$COQTOP/tools/emacs;;
+    -src|--src) COQTOP=$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;;
+    -emacslib|--emacslib) emacslib_spec=yes
+                          emacslib=$2
+			  shift;;
+    -emacs |--emacs) emacs_spec=yes
+		     emacs=$2
+		     shift;;
+    -arch|--arch) arch_spec=yes
+                  arch=$2
+		  shift;;
+    -opt|--opt) bytecamlc=ocamlc.opt
+                nativecamlc=ocamlopt.opt;;
+    -opt-tools|-opttools|--opttools|--opt-tools) byte_opt_tools=opt;;
+    -byte-tools|-bytetools|--bytetools|--byte-tools) byte_opt_tools=byte;;
+    -debug|--debug) coq_debug_flag=-g;;
+    -profile|--profile) coq_profile_flag=-p;;
+    -nowarnings) caml_warnings=" -w a ";;
+     *) echo "Unknown option \"$1\"." 1>&2; exit 2;;
+  esac
+  shift
+done
+
+
+# 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) if test -f /bin/arch ; then
+	    ARCH=`/bin/arch`
+	elif test -f /usr/bin/arch ; then
+	    ARCH=`/usr/bin/arch`
+	elif test -f /usr/ucb/arch ; then
+	    ARCH=`/usr/ucb/arch`
+	elif test -f /bin/uname ; then
+	    ARCH=`/bin/uname -m`
+	else
+	    echo "I can not automatically find the name of your architecture"
+	    echo -n\
+              "Give me a name, please [win32 for Win95, Win98 or WinNT]: "
+	    read ARCH
+	    
+	fi;;
+    yes) ARCH=$arch
+esac
+
+# bindir, libdir, mandir, etc.
+
+case $ARCH in
+  win32)
+	 bindir_def=\\coq\\bin
+	 libdir_def=\\coq\\lib
+	 mandir_def=\\coq\\man
+	 emacslib_def=\\coq\\emacs;;
+  *)
+	 bindir_def=/usr/local/bin
+	 libdir_def=/usr/local/lib/coq
+	 mandir_def=/usr/local/man
+	 emacslib_def=/usr/share/emacs/site-lisp;;
+esac
+
+emacs_def=emacs
+
+case $bindir_spec in
+    no) echo "Where should I install the Coq binaries [$bindir_def] ?"
+        read BINDIR
+	
+	case $BINDIR in
+	    "") BINDIR=$bindir_def;;
+	    *) true;;
+	esac;;
+    yes) BINDIR=$bindir;;
+esac
+
+case $libdir_spec in
+    no) echo "Where should I install the Coq library [$libdir_def] ?"
+        read LIBDIR
+	
+	case $LIBDIR in
+	    "") LIBDIR=$libdir_def;;
+	    *) true;;
+	esac;;
+    yes) LIBDIR=$libdir;;
+esac
+
+case $mandir_spec in
+    no) echo "Where should I install the Coq man pages [$mandir_def] ?"
+        read MANDIR
+	
+	case $MANDIR in
+	    "") MANDIR=$mandir_def;;
+	    *) true;;
+	esac;;
+    yes) MANDIR=$mandir;;
+esac
+
+case $emacslib_spec in
+    no) echo "Where should I install the Coq Emacs mode [$emacslib_def] ?"
+        read EMACSLIB
+	
+	case $EMACSLIB in
+	    "") EMACSLIB=$emacslib_def;;
+	    *) true;;
+	esac;;
+    yes) EMACSLIB=$emacslib;;
+esac
+
+case $emacs_spec in
+    no) echo "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
+
+# 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 \\\\\\\\ocaml/lib/libunix.lib -cclib wsock32.lib";;
+  *) OSDEPLIBS="-cclib -lunix"
+esac
+
+# OS dependent camlp4 options for native compilation
+
+case $ARCH in
+  ppc) OSDEPP4OPTFLAGS="-split_gext";;
+  *) OSDEPP4OPTFLAGS=""
+esac
+
+#the caml str library
+
+case $ARCH in
+    win32) WITH_STR="-cclib \\\\\\\\ocaml/lib/libstr.lib";;
+    *) WITH_STR="-cclib -lstr"
+esac
+
+# executable extension
+
+case $ARCH in
+    win32) EXE=".exe";;
+    *) EXE=""
+esac
+
+# ostype unix versus win32
+
+case $ARCH in
+    win32) OSTYPE="Win32";;
+    *) OSTYPE="Unix"
+esac
+
+# Objective Caml programs
+
+CAMLC=`which ocamlc`
+case $CAMLC in
+	"") echo "ocamlc is not present in your path !"
+	echo "Give me manually the path to the ocamlc executable [/usr/local/bin by default]: "
+	read CAMLC
+	
+	case $CAMLC in
+		"") CAMLC=/usr/local/bin/ocamlc;;
+		*/ocamlc) true;;
+		*/) CAMLC=${CAMLC}ocamlc;;
+		*) CAMLC=${CAMLC}/ocamlc;;
+	esac;;
+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
+
+CAMLBIN=`dirname $CAMLC`
+CAMLVERSION=`$CAMLC -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' `
+
+case $CAMLVERSION in
+  1.*|2.00)
+	echo "Your version of Objective-Caml is $CAMLVERSION."
+	echo "You need Objective-Caml 2.01 or later !"
+	echo "Configuration script failed!"
+	exit 1;;
+  ?*)	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
+
+# do we have a native compiler: test of ocamlopt
+
+CAMLOPT=`which ocamlopt`
+case $CAMLOPT in
+	"") byte_opt_tools=byte;;
+esac
+
+# For Dynlink
+
+CAMLLIB=`ocamlc -v | sed -n -e 's|.*directory:* *\(.*\)$|\1|p' `
+
+# Camlp4
+
+CAMLP4=`which camlp4`
+case $CAMLP4 in
+	"") echo "camlp4 is not present in your path !"
+	echo "Give me manually the path to the camlp4 executable [/usr/local/bin by default]: "
+	read CAMLP4
+	
+	case $CAMLP4 in
+		"") CAMLP4=/usr/local/bin/camlp4;;
+		*/camlp4) true;;
+		*/) CAMLP4=${CAMLP4}camlp4;;
+		*) CAMLP4=${CAMLP4}/camlp4;;
+	esac;;
+esac
+
+if test ! -f $CAMLP4 ; then
+	echo "I can not find the executable '$CAMLP4'! (Have you installed it?)"
+	echo "Configuration script failed!"
+	exit 1
+fi
+
+CAMLP4BIN=`dirname $CAMLP4`
+CAMLP4VERSION=`$CAMLP4 -v 2>&1 | sed -n -e 's|.*version *\(.*\)$|\1|p'`
+case $CAMLP4VERSION in
+  0.*|1.*|2.00*)
+        echo "Your version of Camlp4 is $CAMLP4VERSION."
+	echo "You need Camlp4 2.01 or later !"
+	echo "Configuration script failed!"
+	exit 1;;
+  ?*)	echo "You have Camlp4 $CAMLP4VERSION. Good!";;
+  *) echo "I found Camlp4 but cannot find its version number!"
+     echo "Is it installed properly ?"
+     echo "Configuration script failed!"
+     exit 1;;
+esac
+case $ARCH in
+    win32)
+	CAMLP4LIB=`$CAMLP4 -where |sed -e 's|\\\|/|g'`;;
+    *)
+	CAMLP4LIB=`$CAMLP4 -where`;;
+esac
+
+case $ARCH in
+    win32)
+	STRIPCOMMAND="true";;
+    *)
+	STRIPCOMMAND="strip";;
+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 "  OS dependant libraries         : $OSDEPLIBS"
+echo "  Objective-Caml version         : $CAMLVERSION"
+echo "  Objective-Caml binaries in     : $CAMLBIN"
+echo "  Objective-Caml library in      : $CAMLLIB"
+echo "  Camlp4 version                 : $CAMLP4VERSION"
+echo "  Camlp4 binaries in             : $CAMLP4BIN"
+echo "  Camlp4 library in              : $CAMLP4LIB"
+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 "    emacs mode will be copied in $EMACSLIB"
+echo ""
+
+# Building the $COQTOP/config/Makefile file
+
+rm -f $COQTOP/config/Makefile
+
+case $ARCH in
+    win32)
+	sed -e "s|COQTOPDIRECTORY|$COQTOP|" \
+	    -e "s|COQVERSION|$VERSION|" \
+	    -e "s|BINDIRDIRECTORY|`echo $BINDIR |sed -e 's|\\\|/|g'`|" \
+	    -e "s|COQLIBDIRECTORY|`echo $LIBDIR |sed -e 's|\\\|/|g'`|" \
+	    -e "s|MANDIRDIRECTORY|`echo $MANDIR |sed -e 's|\\\|/|g'`|" \
+	    -e "s|EMACSLIBDIRECTORY|`echo $EMACSLIB |sed -e 's|\\\|/|g'`|" \
+	    -e "s|EMACSCOMMAND|$EMACS|" \
+	    -e "s|ARCHITECTURE|$ARCH|" \
+	    -e "s|OSDEPENDANTLIBS|$OSDEPLIBS|" \
+	    -e "s|OSDEPENDANTP4OPTFLAGS|$OSDEPP4OPTFLAGS|" \
+	    -e "s|STRLIBRARY|$WITH_STR|" \
+	    -e "s|CAMLBINDIRECTORY|$CAMLBIN|" \
+	    -e "s|CAMLP4BINDIRECTORY|$CAMLP4BIN|" \
+	    -e "s|CAMLP4LIBDIRECTORY|$CAMLP4LIB|" \
+	    -e "s|OSKIND|$OSTYPE|" \
+	    -e "s|COQDEBUGFLAG|$coq_debug_flag|" \
+	    -e "s|COQPROFILEFLAG|$coq_profile_flag|" \
+	    -e "s|COQTOOLSFLAG|$byte_opt_tools|" \
+	    -e "s|EXECUTEEXTENSION|$EXE|" \
+	    -e "s|BYTECAMLC|$bytecamlc$caml_warnings $coq_debug_flag|" \
+	    -e "s|NATIVECAMLC|$nativecamlc$caml_warnings|" \
+	    -e "s|STRIPCOMMAND|$STRIPCOMMAND|" \
+	    $COQTOP/config/Makefile.template > $COQTOP/config/Makefile;;
+    *)
+	sed -e "s|COQTOPDIRECTORY|$COQTOP|" \
+	    -e "s|COQVERSION|$VERSION|" \
+	    -e "s|BINDIRDIRECTORY|$BINDIR|" \
+	    -e "s|COQLIBDIRECTORY|$LIBDIR|" \
+	    -e "s|MANDIRDIRECTORY|$MANDIR|" \
+	    -e "s|EMACSLIBDIRECTORY|$EMACSLIB|" \
+	    -e "s|EMACSCOMMAND|$EMACS|" \
+	    -e "s|ARCHITECTURE|$ARCH|" \
+	    -e "s|OSDEPENDANTLIBS|$OSDEPLIBS|" \
+	    -e "s|OSDEPENDANTP4OPTFLAGS|$OSDEPP4OPTFLAGS|" \
+	    -e "s|STRLIBRARY|$WITH_STR|" \
+	    -e "s|CAMLBINDIRECTORY|$CAMLBIN|" \
+	    -e "s|CAMLP4BINDIRECTORY|$CAMLP4BIN|" \
+	    -e "s|CAMLP4LIBDIRECTORY|$CAMLP4LIB|" \
+	    -e "s|OSKIND|$OSTYPE|" \
+	    -e "s|COQDEBUGFLAG|$coq_debug_flag|" \
+	    -e "s|COQPROFILEFLAG|$coq_profile_flag|" \
+	    -e "s|COQTOOLSFLAG|$byte_opt_tools|" \
+	    -e "s|EXECUTEEXTENSION|$EXE|" \
+	    -e "s|BYTECAMLC|$bytecamlc$caml_warnings $coq_debug_flag|" \
+	    -e "s|NATIVECAMLC|$nativecamlc$caml_warnings|" \
+	    -e "s|STRIPCOMMAND|$STRIPCOMMAND|" \
+	    $COQTOP/config/Makefile.template > $COQTOP/config/Makefile;;
+esac
+
+chmod a-w $COQTOP/config/Makefile
+
+# Building the $COQTOP/config/coq_config.ml file
+
+mlconfig_file=$COQTOP/config/coq_config.ml
+rm -f $mlconfig_file
+cat << END_OF_COQ_CONFIG > $mlconfig_file
+(* DO NOT EDIT THIS FILE: automatically generated by ../configure *)
+
+let bindir = "$BINDIR" 
+let coqlib = "$LIBDIR"
+let coqtop = "$COQTOP"
+let camllib = "$CAMLLIB"
+let camlp4lib = "$CAMLP4LIB"
+let arch = "$ARCH"
+let osdeplibs = "$OSDEPLIBS"
+let defined = [ "$OSTYPE" ]
+let version = "$VERSION"
+let versionsi = "$VERSIONSI"
+let date = "$DATE"
+let compile_date = "$COMPILEDATE"
+
+END_OF_COQ_CONFIG
+
+# Subdirectories of theories/ added in coq_config.ml
+subdirs () {
+    (cd $1; find . -type d ! -name CVS ! -name . -exec printf "\"%s\";\n" {} \; >> $mlconfig_file)
+}
+
+echo_e () {
+    case "`uname -s`" in
+	OSF1|SunOS )
+	echo $*;;
+    *)
+	echo -e $*;;
+  esac
+}
+
+echo_e "\nlet theories_dirs = [" >> $mlconfig_file
+subdirs theories
+echo_e "]\n" >> $mlconfig_file
+
+
+if test $ARCH = "win32" ; then
+# We change: / -> \\ and \ -> \\ (dos paths)
+# This is a bit tricky
+sed -e "s|\\\\\\\\\\\\\\\|\\\|" -e "s|/|\\\|g"  -e "s|\\\|\\\\\\\|g" $mlconfig_file > $mlconfig_file.win
+mv $mlconfig_file.win $mlconfig_file
+fi
+chmod a-w $mlconfig_file
+
+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$
diff --git a/dev/header b/dev/header
new file mode 100644
index 0000000000..aeee5b9e7e
--- /dev/null
+++ b/dev/header
@@ -0,0 +1,10 @@
+(****************************************************************************)
+(*                                                                          *)
+(*                          The Coq Proof Assistant                         *)
+(*                                                                          *)
+(*                                 Projet Coq                               *)
+(*                                                                          *)
+(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
+(*              Rocquencourt         Orsay          Lyon                    *)
+(*                                                                          *)
+(****************************************************************************)
diff --git a/kernel/names.ml b/kernel/names.ml
new file mode 100644
index 0000000000..af7f1f7195
--- /dev/null
+++ b/kernel/names.ml
@@ -0,0 +1,249 @@
+
+(* $Id$ *)
+
+open Pp
+open Util
+
+(* Identifiers *)
+
+type identifier = {
+  atom : string ; 
+  index : int }
+
+type name = Name of identifier | Anonymous
+
+let make_ident sa n = { atom = sa; index = n }
+let repr_ident { atom = sa; index = n } = (sa,n)
+
+let string_of_id { atom = s; index = n } =
+  s ^ (if n = -1 then "" else string_of_int n)
+
+let code_of_0 = Char.code '0'
+let code_of_9 = Char.code '9'
+
+let id_of_string s =
+  let slen = String.length s in
+  (* [n'] is the position of the first non nullary digit *)
+  let rec numpart n n' =
+    if n = 0 then 
+      failwith ("identifier " ^ s ^ " cannot be split")
+    else 
+      let c = Char.code (String.get s (n-1)) in
+      if c = code_of_0 && n <> slen then 
+	numpart (n-1) n' 
+      else if code_of_0 <= c && c <= code_of_9 then 
+	numpart (n-1) (n-1)
+      else 
+	n'
+  in
+  let numstart = numpart slen slen in
+  if numstart = slen then 
+    { atom = s; index = -1 } 
+  else
+    { atom = String.sub s 0 numstart;
+      index = int_of_string (String.sub s numstart (slen - numstart)) }
+
+let atompart_of_id id = id.atom
+let index_of_id id = id.index
+
+let explode_id { atom = s; index = n } =
+  (explode s) @ (if n = -1 then [] else explode (string_of_int n))
+
+let print_id { atom = a; index = n } = 
+  match (a,n) with
+    | ("",-1) -> [< 'sTR"[]" >]
+    | ("",n)  -> [< 'sTR"[" ; 'iNT n ; 'sTR"]" >]
+    | (s,n)   -> [< 'sTR s ; (if n = (-1) then [< >] else [< 'iNT n >]) >]
+
+let pr_idl idl = prlist_with_sep pr_spc print_id idl
+
+let id_ord id1 id2 =
+  let (s1,n1) = repr_ident id1
+  and (s2,n2) = repr_ident id2 in
+  let s_bit = Pervasives.compare s1 s2 in
+  if s_bit = 0 then n1 - n2 else s_bit
+
+let id_without_number id = id.index = (-1)
+
+
+(* Fresh names *)
+
+let lift_ident { atom = str; index = i } = { atom = str; index = i+1 }
+
+let next_ident_away ({atom=str} as id) avoid = 
+  let rec name_rec i =
+    let create = if i = (-1) then id else {atom=str;index=i} in
+    if List.mem create avoid then name_rec (i+1) else create
+  in 
+  name_rec (-1)
+
+let rec next_ident_away_from {atom=str;index=i} avoid = 
+  let rec name_rec i =
+    let create = {atom=str;index=i} in
+    if List.mem create avoid then name_rec (i+1) else create
+  in 
+  name_rec i 
+
+let next_name_away_with_default default name l = 
+  match name with
+    | Name(str) -> next_ident_away str l
+    | Anonymous -> next_ident_away (id_of_string default) l
+
+let next_name_away name l = 
+  match name with
+    | Name(str) -> next_ident_away str l
+    | Anonymous -> id_of_string "_"
+
+(* returns lids@[i1..in] where i1..in are new identifiers prefixed id *)
+let get_new_ids n id lids  =
+  let rec get_rec n acc =
+    if n = 0 then 
+      acc 
+    else 
+      let nid = next_ident_away id (acc@lids) in
+      get_rec (n-1) (nid::acc) 
+  in 
+  get_rec n []
+
+
+(* Kinds *)
+
+type path_kind = CCI | FW | OBJ
+
+let string_of_kind = function
+  | CCI -> "cci" 
+  | FW -> "fw" 
+  | OBJ -> "obj"
+
+let kind_of_string = function
+  | "cci" -> CCI 
+  | "fw" -> FW 
+  | "obj" -> OBJ
+  | _ -> invalid_arg "kind_of_string"
+
+
+(* Section paths *)
+
+type section_path = {
+  dirpath : string list ;
+  basename : identifier ;
+  kind : path_kind }
+
+let make_path pa id k = { dirpath = pa; basename = id; kind = k }
+let repr_path { dirpath = pa; basename = id; kind = k} = (pa,id,k)
+
+let kind_of_path sp = sp.kind
+let basename sp = sp.basename
+let dirpath sp = sp.dirpath
+
+let string_of_path_mind sp id =
+  let (sl,_,k) = repr_path sp in
+  implode
+    (List.flatten 
+       (List.map (fun s -> ["#";s]) (List.rev (string_of_id id :: sl)))
+     @ [ "."; string_of_kind k ])
+    
+let string_of_path sp = string_of_path_mind sp sp.basename
+
+let path_of_string s =
+  try
+    let (sl,s,k) = parse_section_path s in
+    make_path (List.rev sl) (id_of_string s) (kind_of_string k)
+  with
+    | Invalid_argument _ -> invalid_arg "path_of_string"
+
+
+let coerce_path k { dirpath = p; basename = id } =
+  { dirpath = p; basename = id; kind = k }
+
+let ccisp_of_fwsp = function
+  | { dirpath = p; basename = id; kind = FW } -> 
+      { dirpath = p; basename = id; kind = CCI }
+  | _ -> invalid_arg "ccisp_of_fwsp"
+
+let ccisp_of { dirpath = p; basename = id } =
+  { dirpath = p; basename = id; kind = CCI }
+
+let objsp_of { dirpath = p; basename = id } =
+  { dirpath = p; basename = id; kind = OBJ }
+
+let fwsp_of_ccisp = function
+  | { dirpath = p; basename = id; kind = CCI } -> 
+      { dirpath = p; basename = id; kind = FW }
+  | _ -> invalid_arg "fwsp_of_ccisp"
+
+let fwsp_of { dirpath = p; basename = id } =
+  { dirpath = p; basename = id; kind = FW }
+
+let append_to_path sp str =
+  let (sp,id,k) = repr_path sp in
+  make_path sp (id_of_string ((string_of_id id)^str)) k
+
+let sp_ord sp1 sp2 =
+  let (p1,id1,k) = repr_path sp1
+  and (p2,id2,k') = repr_path sp2 in
+  let ck = compare k k' in
+  if ck = 0 then
+    let p_bit = compare p1 p2 in
+    if p_bit = 0 then id_ord id1 id2 else p_bit
+  else
+    ck
+
+let sp_gt (sp1,sp2) = sp_ord sp1 sp2 > 0
+
+module SpOrdered =
+  struct
+    type t = section_path
+    let compare = sp_ord
+  end
+
+module Spset = Set.Make(SpOrdered)
+
+(* Hash-consing of name objects *)
+module Hident = Hashcons.Make(
+  struct 
+    type t = identifier
+    type u = string -> string
+    let hash_sub hstr id =
+      { atom = hstr id.atom; index = id.index }
+    let equal id1 id2 = id1.atom == id2.atom && id1.index = id2.index
+    let hash = Hashtbl.hash
+  end)
+
+module Hname = Hashcons.Make(
+  struct 
+    type t = name
+    type u = identifier -> identifier
+    let hash_sub hident = function
+      | Name id -> Name (hident id)
+      | n -> n
+    let equal n1 n2 =
+      match (n1,n2) with
+	| (Name id1, Name id2) -> id1 == id2
+        | (Anonymous,Anonymous) -> true
+        | _ -> false
+    let hash = Hashtbl.hash
+  end)
+
+module Hsp = Hashcons.Make(
+  struct 
+    type t = section_path
+    type u = (identifier -> identifier) * (string -> string)
+    let hash_sub (hident,hstr) sp =
+      { dirpath = List.map hstr sp.dirpath;
+        basename = hident sp.basename;
+        kind = sp.kind }
+    let equal sp1 sp2 =
+      (sp1.basename == sp2.basename) && (sp1.kind = sp2.kind)
+      && (List.length sp1.dirpath = List.length sp2.dirpath)
+      && List.for_all2 (==) sp1.dirpath sp2.dirpath
+    let hash = Hashtbl.hash
+  end)
+
+let hcons_names () =
+  let hstring = Hashcons.simple_hcons Hashcons.Hstring.f () in
+  let hident = Hashcons.simple_hcons Hident.f hstring in
+  let hname = Hashcons.simple_hcons Hname.f hident in
+  let hspcci = Hashcons.simple_hcons Hsp.f (hident,hstring) in
+  let hspfw = Hashcons.simple_hcons Hsp.f (hident,hstring) in
+  (hspcci,hspfw,hname,hident,hstring)
diff --git a/kernel/names.mli b/kernel/names.mli
new file mode 100644
index 0000000000..5445065f7a
--- /dev/null
+++ b/kernel/names.mli
@@ -0,0 +1,65 @@
+
+(* $Id$ *)
+
+open Pp
+
+type identifier
+type name = Name of identifier | Anonymous
+
+val make_ident : string -> int -> identifier
+val string_of_id : identifier -> string
+val id_of_string : string -> identifier
+
+val explode_id : identifier -> string list
+val print_id : identifier -> std_ppcmds
+val pr_idl : identifier list -> std_ppcmds
+val atompart_of_id : identifier -> string
+val index_of_id : identifier -> int
+val id_ord : identifier -> identifier -> int
+val id_without_number : identifier -> bool
+
+
+val lift_ident : identifier -> identifier
+val next_ident_away_from : identifier -> identifier list -> identifier
+val next_ident_away : identifier -> identifier list -> identifier
+val next_name_away : name -> identifier list -> identifier
+val next_name_away_with_default : 
+  string -> name -> identifier list -> identifier
+val get_new_ids : int -> identifier -> identifier list -> identifier list
+
+
+type path_kind = CCI | FW | OBJ
+
+val string_of_kind : path_kind -> string
+val kind_of_string : string -> path_kind
+
+
+type section_path
+
+val make_path : string list -> identifier -> path_kind -> section_path
+val repr_path : section_path -> string list * identifier * path_kind
+val dirpath : section_path -> string list
+val basename : section_path -> identifier
+val kind_of_path : section_path -> path_kind
+
+val path_of_string : string -> section_path
+val string_of_path : section_path -> string
+val string_of_path_mind : section_path -> identifier -> string
+
+val coerce_path : path_kind -> section_path -> section_path
+val fwsp_of : section_path -> section_path
+val ccisp_of : section_path -> section_path
+val objsp_of : section_path -> section_path
+val fwsp_of_ccisp : section_path -> section_path
+val ccisp_of_fwsp : section_path -> section_path
+val append_to_path : section_path -> string -> section_path
+
+val sp_ord : section_path -> section_path -> int
+val sp_gt : section_path * section_path -> bool
+
+module Spset : Set.S with type elt = section_path
+
+(* Hash-consing *)
+val hcons_names : unit ->
+  (section_path -> section_path) * (section_path -> section_path) *
+  (name -> name) * (identifier -> identifier) * (string -> string)
diff --git a/lib/hashcons.ml b/lib/hashcons.ml
new file mode 100644
index 0000000000..301643dbae
--- /dev/null
+++ b/lib/hashcons.ml
@@ -0,0 +1,244 @@
+(****************************************************************************)
+(*                 The Calculus of Inductive Constructions                  *)
+(*                                                                          *)
+(*                                Projet Coq                                *)
+(*                                                                          *)
+(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
+(*              Rocquencourt         Orsay          Lyon                    *)
+(*                                                                          *)
+(*                                 Coq V6.3                                 *)
+(*                               July 1st 1999                              *)
+(*                                                                          *)
+(****************************************************************************)
+(*                               hashcons.ml                                *)
+(****************************************************************************)
+(* Hash consing of datastructures *)
+
+(*
+open Pp;;
+let acces = ref 0;;
+let comparaison = ref 0;;
+let succes = ref 0;;
+let accesstr = ref 0;;
+let comparaisonstr = ref 0;;
+let successtr = ref 0;;
+*)let stat() = ();;
+(*
+  mSGNL [< 'sTR"acces="; 'iNT !acces; 'sPC;
+           'sTR"comp="; 'iNT !comparaison; 'sPC;
+           'sTR"succes="; 'iNT !succes; 'sPC >];
+  comparaison:=0;
+  acces:=0;
+  succes:=0;
+  mSGNL [< 'sTR"String:"; 'sPC;
+           'sTR"acces="; 'iNT !accesstr; 'sPC;
+           'sTR"comp="; 'iNT !comparaisonstr; 'sPC;
+           'sTR"succes="; 'iNT !successtr; 'sPC >];
+  comparaisonstr:=0;
+  accesstr:=0;
+  successtr:=0
+;;
+*)
+
+
+(* The generic hash-consing functions (does not use Obj) *)
+
+(* [t] is the type of object to hash-cons
+ * [u] is the type of hash-cons functions for the sub-structures
+ *   of objects of type t (u usually has the form (t1->t1)*(t2->t2)*...).
+ * [hash_sub u x] is a function that hash-cons the sub-structures of x using
+ *   the hash-consing functions u provides.
+ * [equal] is a comparison function. It is allowed to use physical equality
+ *   on the sub-terms hash-consed by the hash_sub function.
+ * [hash] is the hash function given to the Hashtbl.Make function 
+ *
+ * Note that this module type coerces to the argument of Hashtbl.Make.
+ *)
+module type Comp =
+  sig
+    type t
+    type u
+    val hash_sub :  u -> t -> t
+    val equal : t -> t -> bool
+    val hash : t -> int
+  end
+
+(* The output is a function f such that
+ * [f ()] has the side-effect of creating (internally) a hash-table of the
+ *   hash-consed objects. The result is a function taking the sub-hashcons
+ *   functions and an object, and hashcons it. It does not really make sense
+ *   to call f() with different sub-hcons functions. That's why we use the
+ *   wrappers simple_hcons, recursive_hcons, ... The latter just take as
+ *   argument the sub-hcons functions (the tables are created at that moment),
+ *   and returns the hcons function for t.
+ *)
+module type S =
+  sig
+    type t
+    type u
+    val f : unit -> (u -> t -> t)
+  end
+
+
+module Make(X:Comp) =
+  struct
+    type t = X.t
+    type u = X.u
+
+    (* We create the type of hashtables for t, with our comparison fun.
+     * An invariant is that the table never contains two entries equals
+     * w.r.t (=), although the equality on keys is X.equal. This is
+     * granted since we hcons the subterms before looking up in the table.
+     *)
+    module Htbl = Hashtbl.Make(
+      struct type t=X.t
+             type u=X.u
+             let hash=X.hash
+             let equal x1 x2 = (*incr comparaison;*) X.equal x1 x2
+      end)
+
+    (* The table is created when () is applied.
+     * Hashconsing is then very simple:
+     *  1- hashcons the subterms using hash_sub and u
+     *  2- look up in the table, if we do not get a hit, we add it
+     *)
+    let f () =
+      let tab = Htbl.create 97 in
+        (fun u x ->
+           let y = X.hash_sub u x in
+            (* incr acces;*)
+             try let r = Htbl.find tab y in(* incr succes;*) r
+             with Not_found -> Htbl.add tab y y; y)
+  end;;
+
+(* A few usefull wrappers:
+ * takes as argument the function f above and build a function of type
+ * u -> t -> t that creates a fresh table each time it is applied to the
+ * sub-hcons functions. *)
+
+(* For non-recursive types it is quite easy. *)
+let simple_hcons h u = h () u;;
+
+(* For a recursive type T, we write the module of sig Comp with u equals
+ * to (T -> T) * u0
+ * The first component will be used to hash-cons the recursive subterms
+ * The second one to hashcons the other sub-structures.
+ * We just have to take the fixpoint of h
+ *)
+let recursive_hcons h u =
+  let hc = h () in
+  let rec hrec x = hc (hrec,u) x in
+    hrec
+;;
+
+(* If the structure may contain loops, use this one. *)
+let recursive_loop_hcons h u =
+  let hc = h () in
+  let rec hrec visited x =
+    if List.memq x visited then x
+    else hc (hrec (x::visited),u) x
+  in hrec []
+;;
+
+(* For 2 mutually recursive types *)
+let recursive2_hcons h1 h2 u1 u2 =
+  let hc1 = h1 () in
+  let hc2 = h2 () in
+  let rec hrec1 x = hc1 (hrec1,hrec2,u1) x
+  and hrec2 x = hc2 (hrec1,hrec2,u2) x
+  in (hrec1,hrec2)
+;;
+
+
+
+
+(* A set of global hashcons functions *)
+let hashcons_resets = ref [];;
+let init() = List.iter (fun f -> f()) !hashcons_resets;;
+
+(* [register_hcons h u] registers the hcons function h, result of the above
+ *   wrappers. It returns another hcons function that always uses the same
+ *   table, which can be reinitialized by init()
+ *)
+let register_hcons h u =
+  let hf = ref (h u) in
+  let reset() = hf := h u in
+    hashcons_resets := reset :: !hashcons_resets;
+    (fun x -> !hf x)
+;;
+
+
+
+(* Basic hashcons modules for string and obj. Integers do not need be
+   hashconsed.  *)
+
+(* string *)
+module Hstring = Make(
+  struct
+    type t = string
+    type u = unit
+    let hash_sub () s =(* incr accesstr;*) s
+    let equal s1 s2 =(* incr comparaisonstr;
+      if*) s1=s2(* then (incr successtr; true) else false*)
+    let hash = Hashtbl.hash
+  end);;
+
+(* Obj.t *)
+exception NotEq;;
+
+(* From CAMLLIB/caml/mlvalues.h *)
+let no_scan_tag = 251;;
+let tuple_p obj = Obj.is_block obj & (Obj.tag obj < no_scan_tag);;
+
+let comp_obj o1 o2 =
+  if tuple_p o1 & tuple_p o2 then
+    let n1 = Obj.size o1 and n2 = Obj.size o2 in
+      if n1=n2 then
+        try
+          for i = 0 to pred n1 do
+            if not (Obj.field o1 i == Obj.field o2 i) then raise NotEq
+          done; true
+        with NotEq -> false
+      else false
+  else o1=o2
+;;
+
+let hash_obj hrec o = 
+  begin
+    if tuple_p o then
+      let n = Obj.size o in
+        for i = 0 to pred n do
+          Obj.set_field o i (hrec (Obj.field o i))
+        done
+  end;
+  o
+;;
+
+module Hobj = Make(
+  struct
+    type t = Obj.t
+    type u = (Obj.t -> Obj.t) * unit
+    let hash_sub (hrec,_) = hash_obj hrec
+    let equal = comp_obj
+    let hash = Hashtbl.hash
+  end);;
+
+
+
+(* Hashconsing functions for string and obj. Always use the same
+ * global tables. The latter can be reinitialized with init()
+ *)
+(* string : string -> string *)
+(* obj : Obj.t -> Obj.t *)
+let string = register_hcons (simple_hcons Hstring.f) ();;
+let obj = register_hcons (recursive_hcons Hobj.f) ();;
+
+(* The unsafe polymorphic hashconsing function *)
+let magic_hash (c: 'a) =
+  init();
+  let r = obj (Obj.repr c) in
+    init();
+    (Obj.magic r : 'a)
+;;
+
+(* $Id$ *)
diff --git a/lib/hashcons.mli b/lib/hashcons.mli
new file mode 100644
index 0000000000..76a8fba4e8
--- /dev/null
+++ b/lib/hashcons.mli
@@ -0,0 +1,60 @@
+(****************************************************************************)
+(*                 The Calculus of Inductive Constructions                  *)
+(*                                                                          *)
+(*                                Projet Coq                                *)
+(*                                                                          *)
+(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
+(*              Rocquencourt         Orsay          Lyon                    *)
+(*                                                                          *)
+(*                                 Coq V6.3                                 *)
+(*                               July 1st 1999                              *)
+(*                                                                          *)
+(****************************************************************************)
+(*                               hashcons.mli                               *)
+(****************************************************************************)
+val stat: unit->unit
+
+
+module type Comp =
+  sig
+    type t
+    type u
+    val hash_sub :  u -> t -> t
+    val equal : t -> t -> bool
+    val hash : t -> int
+  end
+
+module type S =
+  sig
+    type t
+    type u
+    val f : unit -> (u -> t -> t)
+  end
+
+module Make(X:Comp): (S with type t = X.t and type u = X.u)
+
+val simple_hcons : (unit -> 'u -> 't -> 't) -> ('u -> 't -> 't)
+val recursive_hcons : (unit -> ('t -> 't) * 'u -> 't -> 't) -> ('u -> 't -> 't)
+val recursive_loop_hcons :
+    (unit -> ('t -> 't) * 'u -> 't -> 't) -> ('u -> 't -> 't)
+val recursive2_hcons :
+  (unit -> ('t1 -> 't1) * ('t2 -> 't2) * 'u1 -> 't1 -> 't1) ->
+    (unit -> ('t1 -> 't1) * ('t2 -> 't2) * 'u2 -> 't2 -> 't2) ->
+      'u1 -> 'u2 -> ('t1 -> 't1) * ('t2 -> 't2)
+
+
+(* Declaring and reinitializing global hash-consing functions *)
+val init : unit -> unit
+val register_hcons : ('u -> 't -> 't) -> ('u -> 't -> 't)
+
+
+module Hstring : (S with type t = string and type u = unit)
+module Hobj : (S with type t = Obj.t and type u = (Obj.t -> Obj.t) * unit)
+
+val string : string -> string
+val obj : Obj.t -> Obj.t
+
+val magic_hash : 'a -> 'a
+
+(* $Id$ *)
+
diff --git a/lib/pp.ml b/lib/pp.ml
new file mode 100644
index 0000000000..0588970bcf
--- /dev/null
+++ b/lib/pp.ml
@@ -0,0 +1,175 @@
+
+(* $Id$ *)
+
+open Pp_control
+
+(* The different kinds of blocks are: 
+   \begin{description}
+   \item[hbox:] Horizontal block no line breaking;
+   \item[vbox:] Vertical block each break leads to a new line;
+   \item[hvbox:] Horizontal-vertical block: same as vbox, except if
+      this block is small enough to fit on a single line
+   \item[hovbox:] Horizontal or Vertical block: breaks lead to new line
+      only when necessary to print the content of the block
+   \item[tbox:] Tabulation block: go to tabulation marks and no line breaking
+      (except if no mark yet on the reste of the line)
+   \end{description}
+ *)
+   
+type block_type =
+  | Pp_hbox of int
+  | Pp_vbox of int
+  | Pp_hvbox of int
+  | Pp_hovbox of int
+  | Pp_tbox
+
+type 'a ppcmd_token =
+  | Ppcmd_print of 'a
+  | Ppcmd_box of block_type * ('a ppcmd_token Stream.t)
+  | Ppcmd_print_break of int * int
+  | Ppcmd_set_tab
+  | Ppcmd_print_tbreak of int * int
+  | Ppcmd_white_space of int
+  | Ppcmd_force_newline
+  | Ppcmd_print_if_broken
+  | Ppcmd_open_box of block_type
+  | Ppcmd_close_box
+  | Ppcmd_close_tbox
+
+type 'a ppdir_token =
+  | Ppdir_ppcmds of 'a ppcmd_token Stream.t
+  | Ppdir_print_newline
+  | Ppdir_print_flush
+
+type std_ppcmds = (int*string) ppcmd_token Stream.t
+type 'a ppdirs = 'a ppdir_token Stream.t
+
+
+(* formatting commands *)
+let sTR s = Ppcmd_print (String.length s,s)
+let sTRas (i,s) = Ppcmd_print (i,s)
+let bRK (a,b) = Ppcmd_print_break (a,b)
+let tBRK (a,b) = Ppcmd_print_tbreak (a,b)
+let tAB = Ppcmd_set_tab
+let fNL = Ppcmd_force_newline
+let pifB = Ppcmd_print_if_broken
+let wS n = Ppcmd_white_space n
+
+(* derived commands *)
+let sPC = Ppcmd_print_break (1,0)
+let cUT = Ppcmd_print_break (0,0)
+let aLIGN = Ppcmd_print_break (0,0)
+let iNT n = sTR (string_of_int n)
+let rEAL r = sTR (string_of_float r)
+let bOOL b = sTR (string_of_bool b)
+let qSTRING s = sTR ("\""^(String.escaped s)^"\"")
+let qS = qSTRING
+
+(* boxing commands *)
+let h n s = [< 'Ppcmd_box(Pp_hbox n,s) >]
+let v n s = [< 'Ppcmd_box(Pp_vbox n,s) >]
+let hV n s = [< 'Ppcmd_box(Pp_hvbox n,s) >]
+let hOV n s = [< 'Ppcmd_box(Pp_hovbox n,s) >]
+let t s = [< 'Ppcmd_box(Pp_tbox,s) >]
+
+(* Opening and closing of boxes *)
+let hB n = Ppcmd_open_box(Pp_hbox n)
+let vB n = Ppcmd_open_box(Pp_vbox n)
+let hVB n = Ppcmd_open_box(Pp_hvbox n)
+let hOVB n = Ppcmd_open_box(Pp_hovbox n)
+let tB = Ppcmd_open_box Pp_tbox
+let cLOSE = Ppcmd_close_box
+let tCLOSE = Ppcmd_close_tbox
+
+
+(* pretty printing functions *)
+let pp_dirs ft = 
+  let maxbox = (get_gp ft).max_depth in
+  let pp_open_box = function
+    | Pp_hbox n   -> Format.pp_open_hbox ft ()
+    | Pp_vbox n   -> Format.pp_open_vbox ft n
+    | Pp_hvbox n  -> Format.pp_open_hvbox ft n
+    | Pp_hovbox n -> Format.pp_open_hovbox ft n
+    | Pp_tbox     -> Format.pp_open_tbox ft () 
+  in
+  let rec pp_cmd = function
+    | Ppcmd_print(n,s)        -> Format.pp_print_as ft n s
+    | Ppcmd_box(bty,ss)       -> (* Prevent evaluation of the stream! *)
+        pp_open_box bty ;
+        if not (Format.over_max_boxes ()) then Stream.iter pp_cmd ss;
+        Format.pp_close_box ft ()
+    | Ppcmd_open_box bty      -> pp_open_box bty
+    | Ppcmd_close_box         -> Format.pp_close_box ft ()
+    | Ppcmd_close_tbox        -> Format.pp_close_tbox ft ()
+    | Ppcmd_white_space n     -> Format.pp_print_break ft n 0
+    | Ppcmd_print_break(m,n)  -> Format.pp_print_break ft m n
+    | Ppcmd_set_tab           -> Format.pp_set_tab ft ()
+    | Ppcmd_print_tbreak(m,n) -> Format.pp_print_tbreak ft m n
+    | Ppcmd_force_newline     -> Format.pp_force_newline ft ()
+    | Ppcmd_print_if_broken   -> Format.pp_print_if_newline ft () 
+  in
+  let pp_dir = function
+    | Ppdir_ppcmds cmdstream -> Stream.iter pp_cmd cmdstream
+    | Ppdir_print_newline    -> Format.pp_print_newline ft ()
+    | Ppdir_print_flush      -> Format.pp_print_flush ft () 
+  in
+  fun dirstream ->
+    try  
+      Stream.iter pp_dir dirstream
+    with 
+      | e -> Format.pp_print_flush ft () ; raise e
+
+
+(* pretty print on stdout and stderr *)
+
+let pp_std_dirs = pp_dirs std_ft
+let pp_err_dirs = pp_dirs err_ft
+
+let pPCMDS x = Ppdir_ppcmds x
+
+(* pretty printing functions WITHOUT FLUSH *)
+let pP_with ft strm =
+  pp_dirs ft [< 'pPCMDS strm >]
+
+let pPNL_with ft strm =
+  pp_dirs ft [< 'pPCMDS [< strm ; 'Ppcmd_force_newline >] >]
+
+let warning_with ft string =
+  pPNL_with ft [< 'sTR"Warning: " ; 'sTR string >]
+
+let wARN_with ft pps =
+  pPNL_with ft [< 'sTR"Warning: " ; pps >]
+
+let pp_flush_with ft =
+  Format.pp_print_flush ft
+
+
+(* pretty printing functions WITH FLUSH *)
+let mSG_with ft strm =
+  pp_dirs ft [< 'pPCMDS strm ; 'Ppdir_print_flush >]
+
+let mSGNL_with ft strm =
+  pp_dirs ft [< 'pPCMDS strm ; 'Ppdir_print_newline >]
+
+let wARNING_with ft strm=
+  pp_dirs ft [<'pPCMDS ([<'sTR "Warning: "; strm>]); 'Ppdir_print_newline>]
+
+
+(* pretty printing functions WITHOUT FLUSH *)
+let pP        = pP_with std_ft
+let pPNL      = pPNL_with std_ft
+let pPERR     = pP_with err_ft
+let pPERRNL   = pPNL_with err_ft
+let message s = pPNL [< 'sTR s >]
+let warning   = warning_with std_ft
+let wARN      = wARN_with std_ft
+let pp_flush  = Format.pp_print_flush std_ft
+let flush_all() = flush stderr; flush stdout; pp_flush()
+
+(* pretty printing functions WITH FLUSH *)
+let mSG = mSG_with std_ft
+let mSGNL = mSGNL_with std_ft
+let mSGERR = mSG_with err_ft
+let mSGERRNL = mSGNL_with err_ft
+let wARNING = wARNING_with std_ft
+
diff --git a/lib/pp.mli b/lib/pp.mli
new file mode 100644
index 0000000000..72bbde1b92
--- /dev/null
+++ b/lib/pp.mli
@@ -0,0 +1,79 @@
+
+(* $Id$ *)
+
+open Pp_control
+
+type 'a ppcmd_token
+
+type std_ppcmds = (int*string) ppcmd_token Stream.t
+
+(* formatting commands *)
+val sTR  : string -> (int*string) ppcmd_token (* string *)
+val sTRas : int * string -> (int*string) ppcmd_token
+                                              (* string with length *)
+val bRK  : int * int -> 'a ppcmd_token        (* break *)
+val tBRK : int * int -> 'a ppcmd_token        (* go to tabulation *)
+val tAB  : 'a ppcmd_token                     (* set tabulation *)
+val fNL  : 'a ppcmd_token                     (* force newline *)
+val pifB : 'a ppcmd_token                     (* print if broken *)
+val wS   : int -> 'a ppcmd_token              (* white space *)
+
+(* derived commands *)
+val sPC     : 'a ppcmd_token                        (* space *)
+val cUT     : 'a ppcmd_token                        (* cut *)
+val aLIGN   : 'a ppcmd_token                        (* go to tab *)
+val iNT     : int -> (int*string) ppcmd_token       (* int *)
+val rEAL    : float -> (int * string) ppcmd_token   (* real *)
+val bOOL    : bool -> (int * string) ppcmd_token    (* bool *)
+val qSTRING : string -> (int * string) ppcmd_token  (* quoted string *)
+val qS      : string -> (int * string) ppcmd_token  (*   "       "   *)
+
+(* boxing commands *)
+val h   : int -> std_ppcmds -> std_ppcmds (* H box   *) 
+val v   : int -> std_ppcmds -> std_ppcmds (* V box   *)
+val hV  : int -> std_ppcmds -> std_ppcmds (* HV box  *)  
+val hOV : int -> std_ppcmds -> std_ppcmds (* HOV box *)
+val t   : std_ppcmds -> std_ppcmds        (* TAB box *)
+
+(* Opening and closing of boxes *)
+val hB    : int -> 'a ppcmd_token  (* open hbox *)
+val vB    : int -> 'a ppcmd_token  (* open vbox *)
+val hVB   : int -> 'a ppcmd_token  (* open hvbox *)
+val hOVB  : int -> 'a ppcmd_token  (* open hovbox *)
+val tB    : 'a ppcmd_token         (* open tbox *)
+val cLOSE : 'a ppcmd_token         (* close box *)
+val tCLOSE: 'a ppcmd_token         (* close tbox *)
+
+
+(* pretty printing functions WITHOUT FLUSH *)
+val pP_with       : Format.formatter -> std_ppcmds -> unit
+val pPNL_with     : Format.formatter -> std_ppcmds -> unit
+val warning_with  : Format.formatter -> string -> unit
+val wARN_with     : Format.formatter -> std_ppcmds -> unit
+val pp_flush_with : Format.formatter -> unit -> unit
+
+(* pretty printing functions WITH FLUSH *)
+val mSG_with      : Format.formatter -> std_ppcmds -> unit
+val mSGNL_with    : Format.formatter -> std_ppcmds -> unit
+
+
+(* These are instances of the previous ones on std_ft and err_ft *)
+
+(* pretty printing functions WITHOUT FLUSH on stdout and stderr *)
+val pP       : std_ppcmds -> unit
+val pPNL     : std_ppcmds -> unit
+val pPERR    : std_ppcmds -> unit
+val pPERRNL  : std_ppcmds -> unit
+val message  : string -> unit       (* = pPNL *)
+val warning  : string -> unit
+val wARN     : std_ppcmds -> unit
+val pp_flush : unit -> unit
+val flush_all: unit -> unit
+
+(* pretty printing functions WITH FLUSH on stdout and stderr *)
+val mSG      : std_ppcmds -> unit
+val mSGNL    : std_ppcmds -> unit
+val mSGERR   : std_ppcmds -> unit
+val mSGERRNL : std_ppcmds -> unit
+val wARNING  : std_ppcmds -> unit
+
diff --git a/lib/pp_control.ml b/lib/pp_control.ml
new file mode 100644
index 0000000000..3eb10e6dde
--- /dev/null
+++ b/lib/pp_control.ml
@@ -0,0 +1,93 @@
+
+(* $Id$ *)
+
+(* Parameters of pretty-printing *)
+
+type pp_global_params = {
+  margin : int;
+  max_indent : int;
+  max_depth : int;
+  ellipsis : string }
+
+(* Default parameters of pretty-printing *)
+
+let dflt_gp = { 
+  margin     = 72;
+  max_indent = 62;
+  max_depth  = 50;
+  ellipsis   = "." }
+
+(* A deeper pretty-printer to print proof scripts *)
+
+let deep_gp = { 
+  margin     = 72;
+  max_indent = 62;
+  max_depth  = 10000;
+  ellipsis   = "." }
+
+(* set_gp : Format.formatter -> pp_global_params -> unit
+ * set the parameters of a formatter *)
+
+let set_gp ft gp = 
+  Format.pp_set_margin ft gp.margin ;
+  Format.pp_set_max_indent ft gp.max_indent ;
+  Format.pp_set_max_boxes ft gp.max_depth ;
+  Format.pp_set_ellipsis_text ft gp.ellipsis
+
+let set_dflt_gp ft = set_gp ft dflt_gp 
+
+let get_gp ft =
+  { margin = Format.pp_get_margin ft ();
+    max_indent = Format.pp_get_max_indent ft ();
+    max_depth = Format.pp_get_max_boxes ft ();
+    ellipsis = Format.pp_get_ellipsis_text ft () }
+
+
+(* Output functions of pretty-printing *)
+
+type 'a pp_formatter_params = {
+  fp_output : out_channel ;
+  fp_output_function : string -> int -> int -> unit ;
+  fp_flush_function : unit -> unit }
+				
+(* Output functions for stdout and stderr *)
+
+let std_fp = {
+  fp_output = stdout ;
+  fp_output_function = output stdout;
+  fp_flush_function = (fun () -> flush stdout) }
+
+let err_fp = {
+  fp_output = stderr ;
+  fp_output_function = output stderr;
+  fp_flush_function = (fun () -> flush stderr) }
+
+(* with_fp : 'a pp_formatter_params -> Format.formatter 
+ * returns of formatter for given formatter functions *)
+
+let with_fp fp =
+  let ft = Format.make_formatter fp.fp_output_function fp.fp_flush_function in
+  Format.pp_set_formatter_out_channel ft fp.fp_output;
+  ft
+
+(* Output on a channel ch *)
+
+let with_output_to ch =
+  let ft = with_fp { fp_output = ch ;
+      	             fp_output_function = (output ch) ;
+	             fp_flush_function = (fun () -> flush ch) } in
+  set_dflt_gp ft; 
+  ft
+
+let std_ft = Format.std_formatter
+let _ = set_dflt_gp std_ft
+
+let err_ft = with_output_to stderr
+
+let deep_ft = with_output_to stdout
+let _ = set_gp deep_ft deep_gp
+
+(* For parametrization through vernacular *)
+let set_depth_boxes v  = Format.pp_set_max_boxes std_ft v
+let get_depth_boxes () = Format.pp_get_max_boxes std_ft ()
+
diff --git a/lib/pp_control.mli b/lib/pp_control.mli
new file mode 100644
index 0000000000..03a1487bf1
--- /dev/null
+++ b/lib/pp_control.mli
@@ -0,0 +1,38 @@
+
+(* $Id$ *)
+
+(* Parameters of pretty-printing *)
+
+type pp_global_params = { 
+  margin : int;
+  max_indent : int;
+  max_depth : int;
+  ellipsis : string }
+
+val dflt_gp : pp_global_params                (* default parameters *)
+val deep_gp : pp_global_params                (* with depth = 10000 *)
+val set_gp : Format.formatter -> pp_global_params -> unit
+val set_dflt_gp : Format.formatter -> unit
+val get_gp : Format.formatter -> pp_global_params
+
+
+(* Output functions of pretty-printing *)
+
+type 'a pp_formatter_params ={ 
+  fp_output : out_channel ;
+  fp_output_function : string -> int -> int -> unit ;
+  fp_flush_function : unit -> unit }
+
+val std_fp : (int*string) pp_formatter_params (* output functions for stdout *)
+val err_fp : (int*string) pp_formatter_params (* output functions for stderr *)
+
+val with_fp : 'a pp_formatter_params -> Format.formatter
+val with_output_to : out_channel -> Format.formatter
+
+val std_ft : Format.formatter  (* the formatter on stdout *)
+val err_ft : Format.formatter  (* the formatter on stderr *)
+val deep_ft : Format.formatter (* a deep formatter on stdout (depth=10000) *)
+
+(* For parametrization through vernacular *)
+val set_depth_boxes : int -> unit
+val get_depth_boxes : unit -> int
diff --git a/lib/util.ml b/lib/util.ml
new file mode 100644
index 0000000000..f04b2cf4b9
--- /dev/null
+++ b/lib/util.ml
@@ -0,0 +1,81 @@
+
+(* $Id$ *)
+
+open Pp
+
+(* Strings *)
+
+let explode s = 
+  let rec explode_rec n =
+    if n >= String.length s then
+      []
+    else 
+      String.make 1 (String.get s n) :: explode_rec (succ n)
+  in 
+  explode_rec 0
+
+let implode sl =
+  let len = List.fold_left (fun a b -> a + (String.length b)) 0 sl in
+  let dest = String.create len in
+  let _ = List.fold_left 
+	    (fun start src ->
+	       let src_len = String.length src in
+	       String.blit src 0 dest start src_len;
+	       start + src_len)
+	    0 sl 
+  in
+  dest
+
+let parse_section_path s =
+  let len = String.length s in
+  let rec decoupe_dirs n =
+    try
+      let pos = String.index_from s n '#' in
+      let dir = String.sub s n (pos-n) in
+      let dirs,n' = decoupe_dirs (succ pos) in
+      dir::dirs,n'
+    with
+      | Not_found -> [],n
+  in
+  let decoupe_kind n =
+    try
+      let pos = String.index_from s n '.' in
+      String.sub s n (pos-n), String.sub s (succ pos) (pred (len-pos))
+    with
+      | Not_found -> invalid_arg "parse_section_path"
+  in
+  if len = 0 || String.get s 0 <> '#' then
+    invalid_arg "parse_section_path"
+  else
+    let dirs,n = decoupe_dirs 1 in
+    let id,k = decoupe_kind n in
+    dirs,id,k
+
+(* Pretty-printing *)
+  
+let pr_spc () = [< 'sPC >];;
+let pr_fnl () = [< 'fNL >];;
+let pr_int n = [< 'iNT n >];;
+let pr_str s = [< 'sTR s >];;
+let pr_coma () = [< 'sTR","; 'sPC >];;
+
+let rec prlist elem l = match l with 
+  | []   -> [< >]
+  | h::t -> let e = elem h and r = prlist elem t in [< e; r >]
+
+let rec prlist_with_sep sep elem l = match l with
+  | []   -> [< >]
+  | [h]  -> elem h
+  | h::t ->
+      let e = elem h and s = sep() and r = prlist_with_sep sep elem t in
+      [< e; s; r >]
+      
+let prvect_with_sep sep elem v =
+  let rec pr n =
+    if n = 0 then 
+      elem v.(0)
+    else 
+      let r = pr (n-1) and s = sep() and e = elem v.(n) in 
+      [< r; s; e >]
+  in
+  if Array.length v = 0 then [< >] else pr (Array.length v - 1)
diff --git a/lib/util.mli b/lib/util.mli
new file mode 100644
index 0000000000..25b419be83
--- /dev/null
+++ b/lib/util.mli
@@ -0,0 +1,25 @@
+
+(* $Id$ *)
+
+open Pp
+
+(* Strings *)
+
+val explode : string -> string list
+val implode : string list -> string
+
+val parse_section_path : string -> string list * string * string
+
+(* Pretty-printing *)
+
+val pr_spc : unit -> std_ppcmds
+val pr_fnl : unit -> std_ppcmds
+val pr_int : int -> std_ppcmds
+val pr_str : string -> std_ppcmds
+val pr_coma : unit -> std_ppcmds
+
+val prlist : ('a -> 'b Stream.t) -> 'a list -> 'b Stream.t
+val prlist_with_sep :
+   (unit -> 'a Stream.t) -> ('b -> 'a Stream.t) -> 'b list -> 'a Stream.t
+val prvect_with_sep :
+   (unit -> 'a Stream.t) -> ('b -> 'a Stream.t) -> 'b array -> 'a Stream.t