From 113b703a695acbe31ac6dd6a8c4aa94f6fda7545 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Mon, 8 Sep 2008 00:15:04 +0200
Subject: Imported Upstream version 8.2~beta4.svn20080907+dfsg

---
 CHANGES                            |  10 ++-
 INSTALL                            |  39 +++++++++
 Makefile                           |  31 ++++---
 Makefile.build                     |  79 +++++++++++-------
 Makefile.common                    |  30 ++++---
 checker/check.ml                   |   8 +-
 checker/checker.ml                 |  10 ++-
 checker/indtypes.ml                |  15 ++++
 checker/mod_checking.ml            | 132 ++++++++++++++---------------
 checker/reduction.ml               |  14 ++++
 checker/safe_typing.ml             |   4 +-
 config/Makefile.template           |   7 +-
 config/coq_config.mli              |   4 +-
 configure                          |  35 ++++++--
 contrib/micromega/coq_micromega.ml |   4 +-
 contrib/subtac/subtac_coercion.ml  |  30 +++----
 dev/base_include                   |   1 +
 dev/db                             |   1 +
 dev/doc/build-system.txt           |   5 +-
 kernel/byterun/coq_fix_code.c      |  10 +--
 kernel/byterun/coq_fix_code.h      |   2 +-
 kernel/byterun/coq_gc.h            |   4 +-
 kernel/byterun/coq_interp.c        |   2 +-
 kernel/byterun/coq_memory.h        |  10 +--
 kernel/byterun/coq_values.h        |   4 +-
 lib/util.ml                        |   4 +-
 man/coq-interface.1                |   4 +-
 man/coq-parser.1                   |  30 +++++++
 man/coq-tex.1                      |  22 ++---
 man/coqdep.1                       |  10 +--
 man/coqdoc.1                       |  38 ++++-----
 man/coqide.1                       | 166 +++++++++++++++++++++++++++++++++++++
 man/coqmktop.1                     |   6 +-
 man/coqwc.1                        |   2 +-
 man/parser.1                       |  30 -------
 parsing/prettyp.ml                 |   4 +-
 parsing/printmod.ml                |  12 +--
 pretyping/classops.ml              | 103 +++++++++++++++--------
 pretyping/classops.mli             |  25 +++---
 pretyping/coercion.ml              |  33 +++-----
 pretyping/reductionops.ml          |   9 +-
 pretyping/reductionops.mli         |  15 ++--
 scripts/coqmktop.ml                |   5 +-
 test-suite/check                   |  16 +++-
 test-suite/success/coercions.v     |  21 +++++
 theories/FSets/FMapFacts.v         |   4 +-
 tools/coqdoc/coqdoc.css            |  15 ++--
 toplevel/class.ml                  |  11 +--
 48 files changed, 728 insertions(+), 348 deletions(-)
 create mode 100644 man/coq-parser.1
 create mode 100644 man/coqide.1
 delete mode 100644 man/parser.1

diff --git a/CHANGES b/CHANGES
index 01a81554..a789796c 100644
--- a/CHANGES
+++ b/CHANGES
@@ -423,6 +423,7 @@ Tools
 - New stand-alone .vo files verifier "coqchk".
 - Extended -I coqtop/coqc option to specify a logical dir: "-I dir -as coqdir".
 - New coqtop/coqc option -exclude-dir to exclude subdirs for option -R.
+- The binary "parser" has been renamed to "coq-parser".
 
 Miscellaneous
 
@@ -432,8 +433,13 @@ Miscellaneous
   Whelp search tool.
 - Syntax of "Test Printing Let ref" and "Test Printing If ref" changed into
   "Test Printing Let for ref" and "Test Printing If for ref".
-- An overhauled build system (new Makefiles); see dev/doc/build-system.txt
-- Add -browser option to configure script
+- An overhauled build system (new Makefiles); see dev/doc/build-system.txt.
+- Add -browser option to configure script.
+- Build a shared library for the C part of Coq, and use it by default.
+  Bytecode executables are now pure. The behaviour is configurable with
+  the -coqrunbyteflags configure option.
+- Complexity tests can be skipped by setting the environment variable
+  COQTEST_SKIPCOMPLEXITY.
 
 Changes from V8.1gamma to V8.1
 ==============================
diff --git a/INSTALL b/INSTALL
index 68cd2faf..626417d6 100644
--- a/INSTALL
+++ b/INSTALL
@@ -2,6 +2,7 @@
             INSTALLATION PROCEDURES FOR THE COQ V8.2 SYSTEM
             -----------------------------------------------
 
+
 WHAT DO YOU NEED ?
 ==================
 
@@ -160,6 +161,10 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
 	Disable the Objective Caml compiler warnings. This option has no
 	effect on the result of the compilation.
 
+-browser <command>
+	Use <command> to open an URL in a browser. %s must appear in <command>,
+	and will be replaced by the URL.
+
 5- Still in the root directory, do
 
 	make world
@@ -249,6 +254,7 @@ THE AVAILABLE COMMANDS.
 
    There is also a tutorial and a FAQ; see http://coq.inria.fr/doc1-eng.html
 
+
 COMMON PROBLEMS.
 ================
 
@@ -263,6 +269,9 @@ COMMON PROBLEMS.
    not be present on certain systems. To fix that, try to replace
    mkdirhier with mkdir -p
 
+    * See also section on dynamically loaded libraries.
+
+
 COMPILING FOR DIFFERENT ARCHITECTURES.
 ======================================
 
@@ -308,3 +317,33 @@ MOVING BINARIES OR LIBRARY.
    the binaries directory) and -libdir (for the standard library directory) :
 
 	coqtop -bindir <new directory> -libdir <new directory>
+
+   See also next section.
+
+
+DYNAMICALLY LOADED LIBRARIES FOR BYTECODE EXECUTABLES.
+======================================================
+
+   Some bytecode executables of Coq use the OCaml runtime, which dynamically
+   loads a shared library (.so or .dll). When it is not installed properly, you
+   can get an error message of this kind:
+
+	Fatal error: cannot load shared library dllcoqrun
+	Reason: dllcoqrun.so: cannot open shared object file: No such file or directory
+
+   In this case, you need either:
+     - to set the CAML_LD_LIBRARY_PATH environment variable to point to the
+       directory where dllcoqrun.so is; this is suitable when you want to run
+       the command a limited number of times in a controlled environment (e.g.
+       during compilation of binary packages);
+     - install dllcoqrun.so in a location listed in the file ld.conf that is in
+       the directory of the standard library of OCaml;
+     - recompile your bytecode executables after reconfiguring the location of
+       of the shared library:
+         ./configure -coqrunbyteflags "-dllib -lcoqrun -dllpath <path>" ...
+       where <path> is the directory where the dllcoqrun.so is installed;
+     - (not recommended) compile bytecode executables with a custom OCaml
+       runtime by using:
+         ./configure -coqrunbyteflags -custom ...
+       be aware that stripping executables generated this way, or performing
+       other executable-specific operations, will make them useless.
diff --git a/Makefile b/Makefile
index 1f770724..1eb7dc85 100644
--- a/Makefile
+++ b/Makefile
@@ -6,7 +6,7 @@
 #         #       GNU Lesser General Public License Version 2.1       #
 #######################################################################
 
-# $Id: Makefile 11309 2008-08-06 10:30:35Z herbelin $ 
+# $Id: Makefile 11387 2008-09-07 21:59:11Z glondu $ 
 
 
 # Makefile for Coq
@@ -24,7 +24,14 @@
 # by Emacs' next-error.
 ###########################################################################
 
-FIND_VCS_CLAUSE:='(' -name '{arch}' -or -name '.svn' -or -name '_darcs' -or -name '.git' -or -name "$${GIT_DIR}" ')' -prune -or
+export FIND_VCS_CLAUSE:='(' \
+  -name '{arch}' -or \
+  -name '.svn' -or \
+  -name '_darcs' -or \
+  -name '.git' -or \
+  -name 'debian' -or \
+  -name "$${GIT_DIR}" \
+')' -prune -type f -or
 FIND_PRINTF_P:=-print | sed 's|^\./||'
 
 export YACCFILES:=$(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.mly' ')' $(FIND_PRINTF_P))
@@ -43,7 +50,7 @@ export MLIFILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.mli' ')' $(FIN
 export ML4FILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.ml4' ')' $(FIND_PRINTF_P))
 #export VFILES   := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.v'   ')' $(FIND_PRINTF_P)) \
 #  $(GENVFILES)
-export CFILES   := $(shell find kernel/byterun -name '*.c')
+export CFILES   := $(shell find kernel/byterun $(FIND_VCS_CLAUSE) -name '*.c')
 
 export ML4FILESML:= $(ML4FILES:.ml4=.ml)
 
@@ -148,12 +155,14 @@ cruftclean: ml4clean
 
 indepclean:
 	rm -f $(GENFILES)
-	rm -f $(COQTOPBYTE) $(COQCBYTE) bin/coq-interface$(EXE) bin/parser$(EXE)
+	rm -f $(COQTOPBYTE) $(COQMKTOPBYTE) $(COQCBYTE) $(CHICKENBYTE)
+	rm -f bin/coq-interface$(EXE) bin/coq-parser$(EXE)
 	find . -name '*~' -or -name '*.cm[ioa]' | xargs rm -f
-	find contrib -name '*.vo' -or -name '*.glob' | xargs rm -f
+	find contrib test-suite -name '*.vo' -or -name '*.glob' | xargs rm -f
 	rm -f */*.pp[iox] contrib/*/*.pp[iox]
 	rm -rf $(SOURCEDOCDIR)
 	rm -f toplevel/mltop.byteml toplevel/mltop.optml
+	rm -f test-suite/check.log
 	rm -f glob.dump
 	rm -f revision
 
@@ -175,11 +184,11 @@ docclean:
 	rm -f doc/coq.tex
 
 archclean: clean-ide cleantheories
-	rm -f $(COQTOPOPT) $(BESTCOQTOP) $(COQC) $(COQMKTOP)
-	rm -f $(COQTOP)  $(COQCOPT) $(COQMKTOPOPT)
-	rm -f bin/parser.opt$(EXE) bin/coq-interface.opt$(EXE)
-	find . -name '*.cmx' -or -name '*.cmxa' -or -name '*.[soa]' | xargs rm -f
-	rm -f $(TOOLS)
+	rm -f $(COQTOPEXE) $(COQMKTOP) $(COQC) $(CHICKEN)
+	rm -f $(COQTOPOPT) $(COQMKTOPOPT) $(COQCOPT) $(CHICKENOPT)
+	rm -f bin/coq-parser.opt$(EXE) bin/coq-interface.opt$(EXE)
+	find . -name '*.cmx' -or -name '*.cmxa' -or -name '*.[soa]' -or -name '*.so' | xargs rm -f
+	rm -f $(TOOLS) $(CSDPCERT)
 
 clean-ide:
 	rm -f $(COQIDECMO) $(COQIDECMX) $(COQIDECMO:.cmo=.cmi) $(COQIDEBYTE) $(COQIDEOPT) $(COQIDE)
@@ -194,7 +203,7 @@ ml4depclean:
 	find . -name '*.ml4.d' | xargs rm -f
 
 depclean:
-	find . -name '*.d' | xargs rm -f
+	find . $(FIND_VCS_CLAUSE) -name '*.d' | xargs rm -f
 
 cleanconfig:
 	rm -f config/Makefile config/coq_config.ml dev/ocamldebug-v7 ide/undo.mli
diff --git a/Makefile.build b/Makefile.build
index a5bae4ea..b8d27b22 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -6,7 +6,7 @@
 #         #       GNU Lesser General Public License Version 2.1       #
 #######################################################################
 
-# $Id: Makefile.build 11309 2008-08-06 10:30:35Z herbelin $ 
+# $Id: Makefile.build 11383 2008-09-07 16:35:13Z glondu $ 
 
 
 # Makefile for Coq
@@ -137,10 +137,11 @@ endif
 
 CINCLUDES= -I $(CAMLHLIB)
 
-# libcoqrun.a 
+# libcoqrun.a, dllcoqrun.so
 
 $(LIBCOQRUN): kernel/byterun/coq_jumptbl.h $(BYTERUN) 
-	$(AR) rc $(LIBCOQRUN) $(BYTERUN) 
+	cd $(dir $(LIBCOQRUN)) && \
+	$(OCAMLMKLIB) -oc $(COQRUN) $(foreach u,$(BYTERUN),$(notdir $(u)))
 	$(RANLIB) $(LIBCOQRUN)
 
 #coq_jumptbl.h is required only if you have GCC 2.0 or later
@@ -180,7 +181,7 @@ $(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN)
 	$(SHOW)'COQMKTOP -o $@'	
 	$(HIDE)$(COQMKTOP) -top $(BYTEFLAGS) -o $@
 
-$(COQTOP): $(ORDER_ONLY_SEP) $(BESTCOQTOP)
+$(COQTOPEXE): $(ORDER_ONLY_SEP) $(BESTCOQTOP)
 	cd bin; ln -sf coqtop.$(BEST)$(EXE) coqtop$(EXE)
 
 LOCALCHKLIBS:=-I checker -I lib -I config -I kernel
@@ -195,7 +196,7 @@ $(CHICKENOPT): checker/check.cmxa checker/main.ml
 
 $(CHICKENBYTE): checker/check.cma checker/main.ml
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) -custom -o $@ unix.cma gramlib.cma checker/check.cma checker/main.ml
+	$(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) -o $@ unix.cma gramlib.cma checker/check.cma checker/main.ml
 
 $(CHICKEN): $(ORDER_ONLY_SEP) $(BESTCHICKEN)
 	cd bin && ln -sf coqchk.$(BEST)$(EXE) coqchk$(EXE)
@@ -204,13 +205,14 @@ $(CHICKEN): $(ORDER_ONLY_SEP) $(BESTCHICKEN)
 
 $(COQMKTOPBYTE): $(COQMKTOPCMO)
 	$(SHOW)'OCAMLC -o $@'	
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ str.cma unix.cma \
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma \
           $(COQMKTOPCMO) $(OSDEPLIBS)
 
 $(COQMKTOPOPT): $(COQMKTOPCMX)
 	$(SHOW)'OCAMLOPT -o $@'	
 	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ str.cmxa unix.cmxa \
           $(COQMKTOPCMX) $(OSDEPLIBS)
+	$(STRIP) $@
 
 $(COQMKTOP): $(ORDER_ONLY_SEP) $(BESTCOQMKTOP)
 	cd bin; ln -sf coqmktop.$(BEST)$(EXE) coqmktop$(EXE)
@@ -226,11 +228,12 @@ scripts/tolink.ml: Makefile.build Makefile.common
 
 $(COQCBYTE): $(COQCCMO) $(COQTOPBYTE) $(BESTCOQTOP)
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ unix.cma $(COQCCMO) $(OSDEPLIBS)
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ unix.cma $(COQCCMO) $(OSDEPLIBS)
 
 $(COQCOPT): $(COQCCMX) $(COQTOPOPT) $(BESTCOQTOP)
 	$(SHOW)'OCAMLOPT -o $@'
 	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ unix.cmxa $(COQCCMX) $(OSDEPLIBS)
+	$(STRIP) $@
 
 $(COQC): $(ORDER_ONLY_SEP) $(BESTCOQC)
 	cd bin; ln -sf coqc.$(BEST)$(EXE) coqc$(EXE)
@@ -361,13 +364,14 @@ contrib/contrib.cmxa: $(CONTRIB:.cmo=.cmx)
 ###########################################################################
 
 ifeq ($(BEST),opt)
-bin/csdpcert$(EXE): $(CSDPCERTCMX)
+contrib/micromega/csdpcert$(EXE): $(CSDPCERTCMX)
 	$(SHOW)'OCAMLOPT -o $@'
 	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) nums.cmxa -o $@ $(CSDPCERTCMX)
+	$(STRIP) $@
 else
-bin/csdpcert$(EXE): $(CSDPCERTCMO)
+contrib/micromega/csdpcert$(EXE): $(CSDPCERTCMO)
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) -custom $(BYTEFLAGS) nums.cma -o $@ $(CSDPCERTCMO)
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) nums.cma -o $@ $(CSDPCERTCMO)
 endif
 
 ###########################################################################
@@ -448,7 +452,7 @@ install-ide-info:
 	$(INSTALLLIB) ide/FAQ $(FULLIDELIB)
 
 ###########################################################################
-# Pcoq: special binaries for debugging (coq-interface, parser)
+# Pcoq: special binaries for debugging (coq-interface, coq-parser)
 ###########################################################################
 
 # target to build Pcoq
@@ -464,12 +468,12 @@ bin/coq-interface.opt$(EXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(INTERFACECMX)
 	$(SHOW)'COQMKTOP -o $@'
 	$(HIDE)$(COQMKTOP) -opt $(OPTFLAGS) -o $@ $(INTERFACECMX)
 
-bin/parser$(EXE):$(LIBCOQRUN) $(PARSERCMO)
+bin/coq-parser$(EXE):$(LIBCOQRUN) $(PARSERCMO)
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) -custom -linkall $(BYTEFLAGS) -o $@ \
+	$(HIDE)$(OCAMLC) $(COQRUNBYTEFLAGS) -linkall $(BYTEFLAGS) -o $@ \
 	  dynlink.cma nums.cma $(LIBCOQRUN) $(CMA) $(PARSERCMO)
 
-bin/parser.opt$(EXE): $(LIBCOQRUN) $(PARSERCMX)
+bin/coq-parser.opt$(EXE): $(LIBCOQRUN) $(PARSERCMX)
 	$(SHOW)'OCAMLOPT -o $@'
 	$(HIDE)$(OCAMLOPT) -linkall $(OPTFLAGS) -o $@ \
 	  $(LIBCOQRUN) nums.cmxa $(CMXA) $(PARSERCMX)
@@ -496,6 +500,10 @@ install-pcoq-manpages:
 # tests
 ###########################################################################
 
+validate:: $(BESTCHICKEN) $(ALLVO)
+	$(SHOW)'COQCHK <theories & contrib>'
+	$(BESTCHICKEN) -boot -o -m $(ALLMODS)
+
 check:: world
 	cd test-suite; \
 	env COQBIN=../bin COQLIB=.. ./check -$(BEST) | tee check.log
@@ -583,27 +591,27 @@ tools:: $(TOOLS) $(DEBUGPRINTERS)
 
 $(COQDEP): $(COQDEPCMO)
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ unix.cma $(COQDEPCMO) $(OSDEPLIBS)
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ unix.cma $(COQDEPCMO) $(OSDEPLIBS)
 
 $(GALLINA): $(GALLINACMO)
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ $(GALLINACMO)
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ $(GALLINACMO)
 
 $(COQMAKEFILE): tools/coq_makefile.cmo config/coq_config.cmo
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ str.cma config/coq_config.cmo tools/coq_makefile.cmo
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma config/coq_config.cmo tools/coq_makefile.cmo
 
 $(COQTEX): tools/coq-tex.cmo
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ str.cma tools/coq-tex.cmo
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma tools/coq-tex.cmo
 
 $(COQWC): tools/coqwc.cmo
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ tools/coqwc.cmo
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ tools/coqwc.cmo
 
 $(COQDOC): $(COQDOCCMO)
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ str.cma unix.cma $(COQDOCCMO)
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma $(COQDOCCMO)
 
 ###########################################################################
 # Installation
@@ -617,7 +625,7 @@ $(COQDOC): $(COQDOCCMO)
   # You must NOT put a "/" at the end (Cygnus for win32 does not like "//").
 
 FULLBINDIR=$(BINDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
-FULLCOQLIB=$(COQLIB:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
+FULLCOQLIB=$(COQLIBINSTALL:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
 FULLMANDIR=$(MANDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
 FULLEMACSLIB=$(EMACSLIB:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
 FULLCOQDOCDIR=$(COQDOCDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
@@ -630,12 +638,12 @@ install-binaries:: install-$(BEST) install-tools
 
 install-byte::
 	$(MKDIR) $(FULLBINDIR)
-	$(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(CSDPCERT) $(FULLBINDIR)
+	$(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(FULLBINDIR)
 	cd $(FULLBINDIR); ln -sf coqtop.byte$(EXE) coqtop$(EXE)
 
 install-opt::
 	$(MKDIR) $(FULLBINDIR)
-	$(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(COQTOPOPT) $(CSDPCERT) $(FULLBINDIR)
+	$(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(COQTOPOPT) $(FULLBINDIR)
 	cd $(FULLBINDIR); ln -sf coqtop.opt$(EXE) coqtop$(EXE)
 
 install-tools::
@@ -655,8 +663,16 @@ install-library:
 	$(MKDIR) $(FULLCOQLIB)/states
 	$(INSTALLLIB) states/*.coq $(FULLCOQLIB)/states
 	$(MKDIR) $(FULLCOQLIB)/user-contrib
-	$(INSTALLLIB) $(LINKCMO) $(LINKCMX) $(GRAMMARCMA) $(FULLCOQLIB)
-	find . -name \*.cmi -exec $(INSTALLLIB) {} $(FULLCOQLIB) \;
+	$(INSTALLLIB) $(LINKCMO) $(GRAMMARCMA) $(FULLCOQLIB)
+ifeq ($(BEST),opt)
+	$(INSTALLLIB) $(LINKCMX) $(FULLCOQLIB)
+endif
+	find . $(FIND_VCS_CLAUSE) -name \*.cmi -exec $(INSTALLLIB) {} $(FULLCOQLIB) \;
+# csdpcert is not meant to be directly called by the user; we install
+# it with libraries
+	-$(MKDIR) -p $(FULLCOQLIB)/contrib/micromega
+	$(INSTALLBIN) $(CSDPCERT) $(FULLCOQLIB)/contrib/micromega
+	$(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB)
 
 install-library-light:
 	$(MKDIR) $(FULLCOQLIB)
@@ -699,7 +715,8 @@ install-latex:
 
 source-doc:
 	if !(test -d $(SOURCEDOCDIR)); then mkdir $(SOURCEDOCDIR); fi
-	$(OCAMLDOC) -html -rectypes $(LOCALINCLUDES) -d $(SOURCEDOCDIR) `find . -name "*.ml"`
+	$(OCAMLDOC) -html -rectypes $(LOCALINCLUDES) -d $(SOURCEDOCDIR) \
+	  `find . $(FIND_VCS_CLAUSE) -name "*.ml"`
 
 
 ###########################################################################
@@ -716,7 +733,7 @@ dev/printers.cma: $(PRINTERSCMO)
 parsing/grammar.cma: $(GRAMMARCMO)
 	$(SHOW)'Testing $@'
 	@touch test.ml4
-	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar
+	$(HIDE)$(OCAMLC) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar
 	@rm -f test-grammar test.*
 	$(SHOW)'OCAMLC -a $@'   
 	$(HIDE)$(OCAMLC) $(BYTEFLAGS) $(GRAMMARCMO) -linkall -a -o $@
@@ -823,8 +840,8 @@ checker/%.cmi: checker/%.mli | checker/%.mli.d
 	$(HIDE)$(OCAMLC) -c $(CHKBYTEFLAGS) $<
 
 %.o: %.c
-	$(SHOW)'CC        $<'
-	$(HIDE)$(CC) -o $@ $(CFLAGS) $(CINCLUDES)  -c $<
+	$(SHOW)'OCAMLC    $<'
+	$(HIDE)cd $(dir $<) && $(OCAMLC) -ccopt "$(CFLAGS)" -c $(notdir $<)
 
 ifdef KEEP_ML4_PREPROCESSED
 .PRECIOUS: %.ml4-preprocessed
@@ -875,8 +892,8 @@ endif
 	$(HIDE)rm -f $*.glob 
 	$(HIDE)$(BOOTCOQTOP) -dump-glob $*.glob -compile $*
 ifdef VALIDATE
-	$(SHOW)'COQCHK    $(shell basename $*)'
-	$(HIDE)$(BESTCHICKEN) -silent -norec $(shell basename $*) \
+	$(SHOW)'COQCHK    $(call vo_to_mod,$@)'
+	$(HIDE)$(BESTCHICKEN) -boot -silent -norec $(call vo_to_mod,$@) \
 	  || ( RV=$$?; rm -f "$@"; exit $${RV} )
 endif
 
diff --git a/Makefile.common b/Makefile.common
index 0a5d4260..a752892d 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -23,7 +23,7 @@ COQC:=bin/coqc$(EXE)
 COQTOPBYTE:=bin/coqtop.byte$(EXE)
 COQTOPOPT:=bin/coqtop.opt$(EXE)
 BESTCOQTOP:=bin/coqtop.$(BEST)$(EXE)
-COQTOP:=bin/coqtop$(EXE)
+COQTOPEXE:=bin/coqtop$(EXE)
 CHICKENBYTE:=bin/coqchk.byte$(EXE)
 CHICKENOPT:=bin/coqchk.opt$(EXE)
 BESTCHICKEN:=bin/coqchk.$(BEST)$(EXE)
@@ -39,14 +39,14 @@ COQIDE:=bin/coqide$(EXE)
 
 ifeq ($(BEST),opt)
 COQBINARIES:= $(COQMKTOP) $(COQC) \
-  $(COQTOPBYTE) $(COQTOPOPT) $(COQTOP) $(CHICKENBYTE) $(CHICKENOPT) $(CHICKEN)
+  $(COQTOPBYTE) $(COQTOPOPT) $(COQTOPEXE) $(CHICKENBYTE) $(CHICKENOPT) $(CHICKEN)
 else
 COQBINARIES:= $(COQMKTOP) $(COQC) \
-  $(COQTOPBYTE)              $(COQTOP) $(CHICKENBYTE)               $(CHICKEN)
+  $(COQTOPBYTE)              $(COQTOPEXE) $(CHICKENBYTE)               $(CHICKEN)
 endif
 OTHERBINARIES:=$(COQMKTOPBYTE) $(COQCBYTE)
 
-CSDPCERT:=bin/csdpcert$(EXE)
+CSDPCERT:=contrib/micromega/csdpcert$(EXE)
 
 ###########################################################################
 # tools
@@ -74,7 +74,7 @@ HEVEA:=hevea
 HEVEAOPTS:=-fix -exec xxdate.exe
 HEVEALIB:=/usr/local/lib/hevea:/usr/lib/hevea
 export TEXINPUTS:=$(COQSRC)/doc:$(HEVEALIB):
-COQTEXOPTS:=-n 72 -image $(COQSRC)/$(COQTOP) -v -sl -small
+COQTEXOPTS:=-n 72 -image $(COQSRC)/$(COQTOPEXE) -v -sl -small
 
 DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex 
 
@@ -111,7 +111,9 @@ REFMANPNGFILES:=$(REFMANEPSFILES:.eps=.png)
 # Object and Source files 
 ###########################################################################
 
-LIBCOQRUN:=kernel/byterun/libcoqrun.a
+COQRUN := coqrun
+LIBCOQRUN:=kernel/byterun/lib$(COQRUN).a
+DLLCOQRUN:=$(dir $(LIBCOQRUN))dll$(COQRUN).so
 
 CLIBS:=unix.cma
 
@@ -377,9 +379,9 @@ PARSERREQUIRES:=$(LINKCMO) $(LIBCOQRUN) # Solution de facilité...
 PARSERREQUIRESCMX:=$(LINKCMX)
 
 ifeq ($(BEST),opt)
-  COQINTERFACE:=bin/coq-interface$(EXE) bin/coq-interface.opt$(EXE) bin/parser$(EXE) bin/parser.opt$(EXE)
+  COQINTERFACE:=bin/coq-interface$(EXE) bin/coq-interface.opt$(EXE) bin/coq-parser$(EXE) bin/coq-parser.opt$(EXE)
 else
-  COQINTERFACE:=bin/coq-interface$(EXE) bin/parser$(EXE)
+  COQINTERFACE:=bin/coq-interface$(EXE) bin/coq-parser$(EXE)
 endif
 
 PARSERCODE:=contrib/interface/line_parser.cmo contrib/interface/vtp.cmo \
@@ -811,6 +813,12 @@ CONTRIBVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) $(RINGVO) $(FIELDVO) \
 ALLVO:= $(INITVO) $(THEORIESVO) $(CONTRIBVO)
 VFILES:= $(ALLVO:.vo=.v)
 
+# convert a (stdlib) filename into a module name:
+# remove .vo, replace theories and contrib by Coq, and replace slashes by dots
+vo_to_mod = $(subst /,.,$(patsubst theories/%,Coq.%,$(patsubst contrib/%,Coq.%,$(1:.vo=))))
+
+ALLMODS:=$(call vo_to_mod,$(ALLVO))
+
 LIBFILES:=$(THEORIESVO) $(CONTRIBVO)
 LIBFILESLIGHT:=$(THEORIESLIGHTVO)
 
@@ -821,10 +829,10 @@ INTERFACEVO:=
 
 MANPAGES:=man/coq-tex.1 man/coqdep.1 man/gallina.1 \
 	man/coqc.1 man/coqtop.1 man/coqtop.byte.1 man/coqtop.opt.1 \
-	man/coqwc.1 man/coqdoc.1 \
+	man/coqwc.1 man/coqdoc.1 man/coqide.1 \
 	man/coq_makefile.1 man/coqmktop.1
 
-PCOQMANPAGES:=man/coq-interface.1 man/parser.1
+PCOQMANPAGES:=man/coq-interface.1 man/coq-parser.1
 
 RECTYPESML:=kernel/term.ml library/nametab.ml proofs/tacexpr.ml \
   parsing/pptactic.ml 
@@ -872,7 +880,7 @@ VO_TARGETS:=logic arith bool narith zarith qarith lists strings sets \
 DOC_TARGETS:=doc doc-html doc-ps doc-pdf stdlib refman tutorial faq rectutorial refman-quick refman-nodep stdlib-nodep
 STAGE3_TARGETS:=world install coqide coqide-files coq coqlib \
   coqlight states pcoq-files check init theories theories-light contrib \
-  $(DOC_TARGETS) $(VO_TARGETS)
+  $(DOC_TARGETS) $(VO_TARGETS) validate
 
 
 # For emacs: 
diff --git a/checker/check.ml b/checker/check.ml
index e91516c7..40ac604e 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -23,8 +23,7 @@ type section_path = {
   dirpath : string list ;
   basename : string }
 let dir_of_path p =
-  make_dirpath
-    (id_of_string p.basename :: List.map id_of_string p.dirpath)
+  make_dirpath (List.map id_of_string p.dirpath)
 let path_of_dirpath dir = 
   match repr_dirpath dir with
       [] -> failwith "path_of_dirpath"
@@ -166,6 +165,9 @@ let remove_load_path dir =
   load_paths := list_filter2 (fun p d -> p <> dir) !load_paths
 
 let add_load_path (phys_path,coq_path) =
+  if !Flags.debug then
+    msgnl (str "path: " ++ pr_dirpath coq_path ++ str " ->" ++ spc() ++
+           str phys_path);
   let phys_path = canonical_path_name phys_path in
     match list_filter2 (fun p d -> p = phys_path) !load_paths with
       | _,[dir] ->
@@ -224,7 +226,7 @@ let locate_qualified_library qid =
       (* Search library in loadpath *)
       if qid.dirpath=[] then get_load_paths ()
       else
-        (* we assume dir is an absolute dirpath *)
+        (* we assume qid is an absolute dirpath *)
         load_paths_of_dir_path (dir_of_path qid)
     in
     if loadpath = [] then raise LibUnmappedDir;
diff --git a/checker/checker.ml b/checker/checker.ml
index 7de25835..1ed094cf 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -191,6 +191,11 @@ let print_usage_channel co command =
 
   -where                 print Coq's standard library location and exit
   -v                     print Coq version and exit
+  -boot                  boot mode
+  -o                     print the list of assumptions
+  -m                     print the maximum heap size
+ 
+  -impredicative-set     set sort Set impredicative
 
   -h, --help             print this list of options
 "
@@ -323,10 +328,9 @@ let parse_args() =
     | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
 
     | ("-v"|"--version") :: _ -> version ()
-
+    | "-boot" :: rem -> boot := true; parse rem	
     | ("-m" | "--memory") :: rem -> Check_stat.memory_stat := true; parse rem
-
-    | ("-o" | "-output-context") :: rem ->
+    | ("-o" | "--output-context") :: rem ->
         Check_stat.output_context := true; parse rem
 
     | "-no-hash-consing" :: rem -> Flags.hash_cons_proofs := false; parse rem
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 8c84fb0f..4c9b3d61 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -19,6 +19,21 @@ open Pp
 open Declarations
 open Environ
 
+let rec debug_string_of_mp = function
+  | MPfile sl -> string_of_dirpath sl
+  | MPbound uid -> "bound("^string_of_mbid uid^")"
+  | MPself uid -> "self("^string_of_msid uid^")"
+  | MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l
+
+let rec string_of_mp = function
+  | MPfile sl -> string_of_dirpath sl
+  | MPbound uid -> string_of_mbid uid
+  | MPself uid -> string_of_msid uid
+  | MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l
+
+let string_of_mp mp =
+  if !Flags.debug then debug_string_of_mp mp else string_of_mp mp
+
 let prkn kn =
   let (mp,_,l) = repr_kn kn in
   str(string_of_mp mp ^ "." ^ string_of_label l)
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index ecf8d633..379273af 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -26,7 +26,7 @@ let refresh_arity ar =
 
 let check_constant_declaration env kn cb =
   Flags.if_verbose msgnl (str "  checking cst: " ++ prcon kn);
-  let env = add_constraints cb.const_constraints env in
+(*  let env = add_constraints cb.const_constraints env in*)
   let env' = check_named_ctxt env cb.const_hyps in
   (match cb.const_type with
       NonPolymorphicType ty ->
@@ -47,58 +47,6 @@ let check_constant_declaration env kn cb =
 (* Checking modules *)
 
 
-let rec add_struct_expr_constraints env = function
-  | SEBident _ -> env
-
-  | SEBfunctor (_,mtb,meb) -> 
-      add_struct_expr_constraints 
-	(add_modtype_constraints env mtb) meb
-
-  | SEBstruct (_,structure_body) ->
-      List.fold_left 
-        (fun env (l,item) -> add_struct_elem_constraints env item)
-        env
-        structure_body
-
-  | SEBapply (meb1,meb2,cst) ->
-(*  let g = Univ.merge_constraints cst Univ.initial_universes in
-msgnl(str"ADDING FUNCTOR APPLICATION CONSTRAINTS:"++fnl()++
-      Univ.pr_universes g++str"============="++fnl());      
-*)
-      Environ.add_constraints cst 
-        (add_struct_expr_constraints 
-	  (add_struct_expr_constraints env meb1) 
-	  meb2)
-  | SEBwith(meb,With_definition_body(_,cb))->
-      Environ.add_constraints cb.const_constraints
-	(add_struct_expr_constraints env meb)
-  | SEBwith(meb,With_module_body(_,_,cst))->
-      Environ.add_constraints cst
-	(add_struct_expr_constraints env meb)	
-		
-and add_struct_elem_constraints env = function 
-  | SFBconst cb -> Environ.add_constraints cb.const_constraints env
-  | SFBmind mib -> Environ.add_constraints mib.mind_constraints env
-  | SFBmodule mb -> add_module_constraints env mb
-  | SFBalias (mp,Some cst) -> Environ.add_constraints cst env
-  | SFBalias (mp,None) -> env
-  | SFBmodtype mtb -> add_modtype_constraints env mtb
-
-and add_module_constraints env mb = 
-  let env = match mb.mod_expr with
-    | None -> env
-    | Some meb -> add_struct_expr_constraints env meb
-  in
-  let env = match mb.mod_type with
-    | None -> env
-    | Some mtb -> 
-	add_struct_expr_constraints env mtb
-  in
-    Environ.add_constraints mb.mod_constraints env
-
-and add_modtype_constraints env mtb = 
-  add_struct_expr_constraints env mtb.typ_expr
-
 exception Not_path
 
 let path_of_mexpr = function
@@ -307,19 +255,18 @@ and check_module_type env mty =
   check_alias mty.typ_alias sub
 
 and check_module env mb =
-  let env' = add_module_constraints env mb in
   let sub =
     match mb.mod_expr, mb.mod_type with
       | None, None -> 
 	  anomaly "Mod_typing.translate_module: empty type and expr in module entry"
-      | None, Some mtb -> check_modexpr env' mtb
+      | None, Some mtb -> check_modexpr env mtb
 
       | Some mexpr, _ -> 
-	  let sub1 = check_modexpr env' mexpr in
+	  let sub1 = check_modexpr env mexpr in
 	  (match mb.mod_type with
 	    | None ->  sub1
 	    | Some mte -> 
-		let sub2 = check_modexpr env' mte in
+		let sub2 = check_modexpr env mte in
                 check_subtypes env
 		  {typ_expr = mexpr;
 		   typ_strength = None;
@@ -342,21 +289,22 @@ and check_structure_field (s,env) mp lab = function
       let mp1 = MPdot(mp,lab) in
       let is_fun, sub = Modops.update_subst env msb mp1 in
       ((if is_fun then s else join s sub),
-       Modops.add_module (MPdot(mp,lab)) msb
-         (add_module_constraints env msb))
+       Modops.add_module (MPdot(mp,lab)) msb env)
   | SFBalias(mp2,cst) ->
+      (* cf Safe_typing.add_alias *)
       (try
+        let mp' = MPdot(mp,lab) in
         let mp2' = scrape_alias mp2 env in
-        let msb = lookup_module mp2' env in
-        (join s (add_mp (MPdot(mp,lab)) mp2' msb.mod_alias),
-         Option.fold_right add_constraints cst
-           (register_alias (MPdot(mp,lab)) mp2 env))
+        let _,sub = Modops.update_subst env (lookup_module mp2' env) mp2' in
+        let sub = update_subst sub (map_mp mp' mp2') in
+        let sub = join_alias sub (map_mp mp' mp2') in
+        let sub = add_mp mp' mp2' sub in
+        (join s sub, register_alias mp' mp2 env)
       with Not_found -> failwith "unkown aliased module")
   | SFBmodtype mty ->
       let kn = MPdot(mp, lab) in
       check_module_type env mty;
-      (join s mty.typ_alias,
-       add_modtype kn mty (add_modtype_constraints env mty))
+      (join s mty.typ_alias, add_modtype kn mty env)
 
 and check_modexpr env mse = match mse with
   | SEBident mp ->
@@ -396,3 +344,57 @@ and check_modexpr env mse = match mse with
         List.fold_left (fun env (lab,mb) ->
           check_structure_field env mp lab mb) (empty_subst,env) msb in
       sub
+
+(*
+let rec add_struct_expr_constraints env = function
+  | SEBident _ -> env
+
+  | SEBfunctor (_,mtb,meb) -> 
+      add_struct_expr_constraints 
+	(add_modtype_constraints env mtb) meb
+
+  | SEBstruct (_,structure_body) ->
+      List.fold_left 
+        (fun env (l,item) -> add_struct_elem_constraints env item)
+        env
+        structure_body
+
+  | SEBapply (meb1,meb2,cst) ->
+(*  let g = Univ.merge_constraints cst Univ.initial_universes in
+msgnl(str"ADDING FUNCTOR APPLICATION CONSTRAINTS:"++fnl()++
+      Univ.pr_universes g++str"============="++fnl());      
+*)
+      Environ.add_constraints cst 
+        (add_struct_expr_constraints 
+	  (add_struct_expr_constraints env meb1) 
+	  meb2)
+  | SEBwith(meb,With_definition_body(_,cb))->
+      Environ.add_constraints cb.const_constraints
+	(add_struct_expr_constraints env meb)
+  | SEBwith(meb,With_module_body(_,_,cst))->
+      Environ.add_constraints cst
+	(add_struct_expr_constraints env meb)	
+		
+and add_struct_elem_constraints env = function 
+  | SFBconst cb -> Environ.add_constraints cb.const_constraints env
+  | SFBmind mib -> Environ.add_constraints mib.mind_constraints env
+  | SFBmodule mb -> add_module_constraints env mb
+  | SFBalias (mp,Some cst) -> Environ.add_constraints cst env
+  | SFBalias (mp,None) -> env
+  | SFBmodtype mtb -> add_modtype_constraints env mtb
+
+and add_module_constraints env mb = 
+  let env = match mb.mod_expr with
+    | None -> env
+    | Some meb -> add_struct_expr_constraints env meb
+  in
+  let env = match mb.mod_type with
+    | None -> env
+    | Some mtb -> 
+	add_struct_expr_constraints env mtb
+  in
+    Environ.add_constraints mb.mod_constraints env
+
+and add_modtype_constraints env mtb = 
+  add_struct_expr_constraints env mtb.typ_expr
+*)
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 49f05daf..c398f0a4 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -195,6 +195,12 @@ let in_whnf (t,stk) =
     | (FFlex _ | FProd _ | FEvar _ | FInd _ | FAtom _ | FRel _) -> true
     | FLOCKED -> assert false
 
+let oracle_order fl1 fl2 =
+  match fl1,fl2 with
+      ConstKey c1, ConstKey c2 -> (*height c1 > height c2*)false
+    | _, ConstKey _ -> true
+    | _ -> false
+
 (* Conversion between  [lft1]term1 and [lft2]term2 *)
 let rec ccnv univ cv_pb infos lft1 lft2 term1 term2 = 
   eqappr univ cv_pb infos (lft1, (term1,[])) (lft2, (term2,[]))
@@ -247,6 +253,14 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
         with NotConvertible ->
           (* else the oracle tells which constant is to be expanded *)
           let (app1,app2) =
+            if oracle_order fl1 fl2 then
+              match unfold_reference infos fl1 with
+                | Some def1 -> ((lft1, whd_stack infos def1 v1), appr2)
+                | None ->
+                    (match unfold_reference infos fl2 with
+                      | Some def2 -> (appr1, (lft2, whd_stack infos def2 v2))
+                     | None -> raise NotConvertible)
+            else
 	      match unfold_reference infos fl2 with
                 | Some def2 -> (appr1, (lft2, whd_stack infos def2 v2))
                 | None ->
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 4b156e7e..d5779923 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -31,7 +31,7 @@ let set_engagement c =
 let full_add_module dp mb digest =
   let env = !genv in
   let mp = MPfile dp in
-  let env = add_module_constraints env mb in
+  let env = add_constraints mb.mod_constraints env in
   let env = Modops.add_module mp mb env in
   genv := add_digest env dp digest
 
@@ -121,7 +121,7 @@ let import file (dp,mb,depends,engmt as vo) digest =
   let env = !genv in
   check_imports msg_warning dp env depends;
   check_engagement env engmt;
-  check_module env mb;
+  check_module (add_constraints mb.mod_constraints env) mb;
   stamp_library file digest;
   (* We drop proofs once checked *)
 (*  let mb = lighten_module mb in*)
diff --git a/config/Makefile.template b/config/Makefile.template
index fc8af173..e0e7bf0b 100644
--- a/config/Makefile.template
+++ b/config/Makefile.template
@@ -21,6 +21,10 @@ COQ_CONFIGURED=yes
 # Local use (no installation)
 LOCAL=LOCALINSTALLATION
 
+# Bytecode link flags for VM ("-custom" or "-dllib -lcoqrun")
+COQRUNBYTEFLAGS=XCOQRUNBYTEFLAGS
+BUILDLDPATH=
+
 # Paths for true installation
 # BINDIR=path where coqtop, coqc, coqmktop, coq-tex, coqdep, gallina and
 #        do_Makefile will reside
@@ -28,7 +32,7 @@ LOCAL=LOCALINSTALLATION
 # MANDIR=path where to install manual pages
 # EMACSDIR=path where to put Coq's Emacs mode (coq.el)
 BINDIR="BINDIRDIRECTORY"
-COQLIB="COQLIBDIRECTORY"
+COQLIBINSTALL="COQLIBDIRECTORY"
 MANDIR="MANDIRDIRECTORY"
 DOCDIR="DOCDIRDIRECTORY"
 EMACSLIB="EMACSLIBDIRECTORY"
@@ -58,6 +62,7 @@ COQIDEINCLUDES=LABLGTKINCLUDES
 # Objective-Caml compile command 
 OCAML="OCAMLEXEC"
 OCAMLC="BYTECAMLC"
+OCAMLMKLIB="OCAMLMKLIBEXEC"
 OCAMLOPT="NATIVECAMLC"
 OCAMLDEP="OCAMLDEPEXEC"
 OCAMLDOC="OCAMLDOCEXEC"
diff --git a/config/coq_config.mli b/config/coq_config.mli
index 3898a0f3..af943509 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: coq_config.mli 11313 2008-08-07 11:15:03Z barras $ i*)
+(*i $Id: coq_config.mli 11380 2008-09-07 12:27:27Z glondu $ i*)
 
 val local : bool        (* local use (no installation) *)
 
@@ -24,6 +24,8 @@ val camlp4lib : string  (* where is the library of Camlp4 *)
 val best : string       (* byte/opt *)
 val arch : string       (* architecture *)
 val osdeplibs : string  (* OS dependant link options for ocamlc *)
+val coqrunbyteflags : string (* -custom/-dllib -lcoqrun *)
+
 
 (* val defined : string list  (* options for lib/ocamlpp *) *)
 
diff --git a/configure b/configure
index 2747ee2f..79a772ed 100755
--- a/configure
+++ b/configure
@@ -6,10 +6,13 @@
 # 
 ##################################
 
-VERSION=8.2beta4
+VERSION=8.2
 VOMAGIC=08193 
 STATEMAGIC=19764
-DATE="Aug. 2008"
+DATE="Jun. 2008"
+
+# Create the bin/ directory if non-existent
+test -d bin || mkdir bin
 
 # a local which command for sh
 which () {
@@ -32,6 +35,8 @@ usage () {
     printf "\tSet installation directory to <dir>\n"
     echo "-local"
     printf "\tSet installation directory to the current source tree\n"
+    echo "-coqrunbyteflags"
+    printf "\tSet link flags for VM-dependent bytecode\n"
     echo "-src"
     printf "\tSpecifies the source directory\n"
     echo "-bindir"
@@ -83,6 +88,7 @@ usage () {
 # Default OCaml binaries
 bytecamlc=ocamlc
 nativecamlc=ocamlopt
+ocamlmklib=ocamlmklib
 ocamlexec=ocaml
 ocamldepexec=ocamldep
 ocamldocexec=ocamldoc
@@ -104,6 +110,7 @@ ar_exec=ar
 ranlib_exec=ranlib
 
 local=false
+coqrunbyteflags_spec=no
 src_spec=no
 prefix_spec=no
 bindir_spec=no
@@ -137,6 +144,9 @@ while : ; do
                       prefix="$2"
 		      shift;;
     -local|--local) local=true;;
+    -coqrunbyteflags|--coqrunbyteflags) coqrunbyteflags_spec=yes
+                                        coqrunbyteflags="$2"
+                                        shift;;
     -src|--src) src_spec=yes
                 COQSRC="$2"
 	        shift;;
@@ -754,6 +764,14 @@ case $coqdocdir_spec/$prefix_spec/$local in
 	esac;;
 esac
 
+BUILDLDPATH="# you might want to set CAML_LD_LIBRARY_PATH by hand!"
+case $coqrunbyteflags_spec/$local in
+    yes/*) COQRUNBYTEFLAGS="$coqrunbyteflags";;
+    */true) COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath $COQTOP/kernel/byterun";;
+    *) COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath $LIBDIR"
+       BUILDLDPATH="export CAML_LD_LIBRARY_PATH=$COQTOP/kernel/byterun";;
+esac
+
 # case $emacs_spec in
 #     no) echo "Which Emacs command should I use to compile coq.el [$emacs_def] ?"
 #         read EMACS
@@ -774,6 +792,7 @@ echo "  Architecture                      : $ARCH"
 if test ! -z "$OS" ; then
   echo "  Operating system                  : $OS"
 fi
+echo "  Coq VM bytecode link flags        : $COQRUNBYTEFLAGS"
 echo "  OS dependent libraries            : $OSDEPLIBS"
 echo "  Objective-Caml/Camlp4 version     : $CAMLVERSION"
 echo "  Objective-Caml/Camlp4 binaries in : $CAMLBIN"
@@ -862,9 +881,10 @@ cat << END_OF_COQ_CONFIG > $mlconfig_file
 (* DO NOT EDIT THIS FILE: automatically generated by ../configure *)
 
 let local = $local
-let bindir = "$ESCBINDIR" 
-let coqlib = "$ESCLIBDIR"
-let coqtop = "$ESCCOQTOP"
+let coqrunbyteflags = "$COQRUNBYTEFLAGS"
+let bindir = try Sys.getenv "COQBIN" with Not_found -> "$ESCBINDIR"
+let coqlib = try Sys.getenv "COQLIB" with Not_found -> "$ESCLIBDIR"
+let coqtop = try Sys.getenv "COQTOP" with Not_found -> "$ESCCOQTOP"
 let camldir = "$ESCCAMLDIR"
 let camllib = "$ESCCAMLLIB"
 let camlp4 = "$CAMLP4"
@@ -909,10 +929,12 @@ chmod a-w "$mlconfig_file"
 rm -f "$COQSRC/config/Makefile"
 
 sed -e "s|LOCALINSTALLATION|$local|" \
+    -e "s|XCOQRUNBYTEFLAGS|$COQRUNBYTEFLAGS|" \
     -e "s|COQSRCDIRECTORY|$COQSRC|" \
     -e "s|COQVERSION|$VERSION|" \
     -e "s|BINDIRDIRECTORY|$ESCBINDIR|" \
     -e "s|COQLIBDIRECTORY|$ESCLIBDIR|" \
+    -e "s|BUILDLDPATH=|$BUILDLDPATH|" \
     -e "s|MANDIRDIRECTORY|$ESCMANDIR|" \
     -e "s|DOCDIRDIRECTORY|$ESCDOCDIR|" \
     -e "s|EMACSLIBDIRECTORY|$ESCEMACSLIB|" \
@@ -937,6 +959,7 @@ sed -e "s|LOCALINSTALLATION|$local|" \
     -e "s|BESTCOMPILER|$best_compiler|" \
     -e "s|EXECUTEEXTENSION|$EXE|" \
     -e "s|BYTECAMLC|$bytecamlc|" \
+    -e "s|OCAMLMKLIBEXEC|$ocamlmklib|" \
     -e "s|NATIVECAMLC|$nativecamlc|" \
     -e "s|OCAMLEXEC|$ocamlexec|" \
     -e "s|OCAMLDEPEXEC|$ocamldepexec|" \
@@ -994,4 +1017,4 @@ echo
 echo "*Warning* To compile the system for a new architecture"
 echo "          don't forget to do a 'make archclean' before './configure'."
 
-# $Id: configure 11320 2008-08-07 19:40:59Z notin $
+# $Id: configure 11380 2008-09-07 12:27:27Z glondu $
diff --git a/contrib/micromega/coq_micromega.ml b/contrib/micromega/coq_micromega.ml
index 02ff61a1..5ae12394 100644
--- a/contrib/micromega/coq_micromega.ml
+++ b/contrib/micromega/coq_micromega.ml
@@ -1193,8 +1193,8 @@ let call_csdpcert provername poly =
   output_value ch_to (provername,poly : provername * micromega_polys);
   close_out ch_to;
   let cmdname =
-    Filename.concat Coq_config.bindir
-      ("csdpcert" ^ Coq_config.exec_extension) in
+    List.fold_left Filename.concat Coq_config.coqlib
+      ["contrib"; "micromega"; "csdpcert" ^ Coq_config.exec_extension] in
   let c = Sys.command (cmdname ^" "^ tmp_to ^" "^ tmp_from) in
   (try Sys.remove tmp_to with _ -> ());
   if c <> 0 then Util.error ("Failed to call csdp certificate generator");
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index b046f0b3..4d8f868f 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -6,7 +6,7 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(* $Id: subtac_coercion.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
+(* $Id: subtac_coercion.ml 11343 2008-09-01 20:55:13Z herbelin $ *)
 
 open Util
 open Names
@@ -310,8 +310,6 @@ module Coercion = struct
 
   (* Typing operations dealing with coercions *)
 
-  let class_of1 env sigma t = class_of env sigma (nf_evar sigma t)
-
   (* Here, funj is a coercion therefore already typed in global context *)
   let apply_coercion_args env argl funj =
     let rec apply_rec acc typ = function
@@ -339,19 +337,17 @@ module Coercion = struct
 
   (* raise Not_found if no coercion found *)
   let inh_pattern_coerce_to loc pat ind1 ind2 =
-    let i1 = inductive_class_of ind1 in
-    let i2 = inductive_class_of ind2 in
-    let p = lookup_pattern_path_between (i1,i2) in
+    let p = lookup_pattern_path_between (ind1,ind2) in
       apply_pattern_coercion loc pat p
 
   (* appliquer le chemin de coercions p à hj *)
 
-  let apply_coercion env p hj typ_cl =
+  let apply_coercion env sigma p hj typ_cl =
     try 
       fst (List.fold_left
              (fun (ja,typ_cl) i -> 
 		let fv,isid = coercion_value i in
-		let argl = (class_args_of typ_cl)@[ja.uj_val] in
+		let argl = (class_args_of env sigma typ_cl)@[ja.uj_val] in
 		let jres = apply_coercion_args env argl fv in
 		  (if isid then 
 		     { uj_val = ja.uj_val; uj_type = jres.uj_type }
@@ -370,9 +366,9 @@ module Coercion = struct
 	      (isevars',{ uj_val = j.uj_val; uj_type = t })
 	| _ ->
        	    (try
- 	       let t,i1 = class_of1 env (evars_of isevars) j.uj_type in
-      	       let p = lookup_path_to_fun_from i1 in
-		 (isevars,apply_coercion env p j t)
+      	       let t,p =
+		 lookup_path_to_fun_from env (evars_of isevars) j.uj_type in
+		 (isevars,apply_coercion env (evars_of isevars) p j t)
 	     with Not_found ->
 	       try 
 		 let coercef, t = mu env isevars t in
@@ -382,9 +378,8 @@ module Coercion = struct
 
   let inh_tosort_force loc env isevars j =
     try
-      let t,i1 = class_of1 env (evars_of isevars) j.uj_type in
-      let p = lookup_path_to_sort_from i1 in
-      let j1 = apply_coercion env p j t in 
+      let t,p = lookup_path_to_sort_from env (evars_of isevars) j.uj_type in
+      let j1 = apply_coercion env (evars_of isevars) p j t in 
 	(isevars,type_judgment env (j_nf_evar (evars_of isevars) j1))
     with Not_found ->
       error_not_a_type_loc loc env (evars_of isevars) j
@@ -417,12 +412,11 @@ module Coercion = struct
     else
     let v', t' =
       try 
-	let t1,i1 = class_of1 env (evars_of evd) c1 in
-	let t2,i2 = class_of1 env (evars_of evd) t in
-	let p = lookup_path_between (i2,i1) in
+	let t2,t1,p = lookup_path_between env (evars_of evd) (t,c1) in
 	  match v with
 	      Some v -> 
-		let j = apply_coercion env p {uj_val = v; uj_type = t} t2 in
+		let j = apply_coercion env (evars_of evd) p
+		  {uj_val = v; uj_type = t} t2 in
 		  Some j.uj_val, j.uj_type
 	    | None -> None, t
       with Not_found -> raise NoCoercion 
diff --git a/dev/base_include b/dev/base_include
index 398f60d2..0b7a0b67 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -29,6 +29,7 @@
 #install_printer  (* qualid *)  ppqualid;;
 #install_printer  (* kernel_name *) ppkn;;
 #install_printer  (* constant *) ppcon;;
+#install_printer  (* cl_index *) ppclindex;;
 #install_printer  (* constr *)  print_pure_constr;; 
 #install_printer  (* patch *) ppripos;;
 #install_printer  (* values *) ppvalues;;
diff --git a/dev/db b/dev/db
index 6221462a..81878570 100644
--- a/dev/db
+++ b/dev/db
@@ -13,6 +13,7 @@ install_printer Top_printers.ppkn
 install_printer Top_printers.ppcon
 install_printer Top_printers.ppsp
 install_printer Top_printers.ppqualid
+install_printer Top_printers.ppclindex
 install_printer Top_printers.ppbigint
 
 install_printer Top_printers.pppattern
diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt
index c9571f7c..9362aeeb 100644
--- a/dev/doc/build-system.txt
+++ b/dev/doc/build-system.txt
@@ -253,9 +253,8 @@ config/Makefile looks like it contains a lot of unused variables,
 clean that up (are any maybe used by nightly scripts on
 pauillac?). Also, the COQTOP variable from config/Makefile (and used
 in contribs) has a very poorly chosen name, because "coqtop" is the
-name of a Coq executable! For example, in the Coq makefile it is
-immediately clobbered by "bin/coqtop$(EXE)"! Rename it to COQROOT or
-COQTREE or COQDIR or ...
+name of a Coq executable! In the coq Makefiles, $(COQTOPEXE) is used
+to refer to that executable.
 
 Promote the granular .glob handling to official way of doing things
 for Coq developments, that is implement it in coq_makefile and the
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 55b907ad..5d302660 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -13,11 +13,11 @@
 
 #include <stdio.h>
 #include <stdlib.h> 
-#include <config.h>
-#include <misc.h>
-#include <mlvalues.h>
-#include <fail.h>
-#include <memory.h>
+#include <caml/config.h>
+#include <caml/misc.h>
+#include <caml/mlvalues.h>
+#include <caml/fail.h>
+#include <caml/memory.h>
 #include "coq_instruct.h"
 #include "coq_fix_code.h"
 
diff --git a/kernel/byterun/coq_fix_code.h b/kernel/byterun/coq_fix_code.h
index 00345318..c1a4e0ae 100644
--- a/kernel/byterun/coq_fix_code.h
+++ b/kernel/byterun/coq_fix_code.h
@@ -12,7 +12,7 @@
 #ifndef _COQ_FIX_CODE_
 #define _COQ_FIX_CODE_
 
-#include <mlvalues.h>
+#include <caml/mlvalues.h>
 void * coq_stat_alloc (asize_t sz);
 
 #ifdef THREADED_CODE
diff --git a/kernel/byterun/coq_gc.h b/kernel/byterun/coq_gc.h
index ccccbe78..c7b18b90 100644
--- a/kernel/byterun/coq_gc.h
+++ b/kernel/byterun/coq_gc.h
@@ -10,8 +10,8 @@
 
 #ifndef _COQ_CAML_GC_
 #define _COQ_CAML_GC_
-#include <mlvalues.h>
-#include <alloc.h>
+#include <caml/mlvalues.h>
+#include <caml/alloc.h>
 
 typedef void (*scanning_action) (value, value *);
 
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 880e978a..98ef2791 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -21,7 +21,7 @@
 #include "coq_values.h" 
 
 /*spiwack : imports support functions for 64-bit integers */
-#include "config.h"
+#include <caml/config.h>
 #ifdef ARCH_INT64_TYPE
 #include "int64_native.h"
 #else
diff --git a/kernel/byterun/coq_memory.h b/kernel/byterun/coq_memory.h
index edd05948..c0093a49 100644
--- a/kernel/byterun/coq_memory.h
+++ b/kernel/byterun/coq_memory.h
@@ -11,11 +11,11 @@
 #ifndef _COQ_MEMORY_
 #define _COQ_MEMORY_
 
-#include <config.h>
-#include <fail.h>
-#include <misc.h>
-#include <memory.h>
-#include <mlvalues.h>
+#include <caml/config.h>
+#include <caml/fail.h>
+#include <caml/misc.h>
+#include <caml/memory.h>
+#include <caml/mlvalues.h>
 
 
 #define Coq_stack_size (4096 * sizeof(value))
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
index 4c631fce..1bf493e2 100644
--- a/kernel/byterun/coq_values.h
+++ b/kernel/byterun/coq_values.h
@@ -11,8 +11,8 @@
 #ifndef _COQ_VALUES_
 #define _COQ_VALUES_
 
-#include <alloc.h>
-#include <mlvalues.h>
+#include <caml/alloc.h>
+#include <caml/mlvalues.h>
 
 #define Default_tag 0
 #define Accu_tag 0
diff --git a/lib/util.ml b/lib/util.ml
index 75ee4246..a19cc65b 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id: util.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: util.ml 11350 2008-09-02 15:37:49Z barras $ *)
 
 open Pp
 
@@ -1361,7 +1361,7 @@ let heap_size () =
   let stat = Gc.stat ()
   and control = Gc.get () in
   let max_words_total = stat.Gc.heap_words + control.Gc.minor_heap_size in
-  (max_words_total * Sys.word_size / 8)
+  (max_words_total * (Sys.word_size / 8))
 
 let heap_size_kb () = (heap_size () + 1023) / 1024
 
diff --git a/man/coq-interface.1 b/man/coq-interface.1
index 2ab2bf95..ee013d95 100644
--- a/man/coq-interface.1
+++ b/man/coq-interface.1
@@ -1,7 +1,7 @@
 .TH COQ 1 "April 25, 2001"
 
 .SH NAME
-coq-interface \-
+coq\-interface \- Customized Coq toplevel to make user interfaces
 
 
 .SH SYNOPSIS
@@ -29,7 +29,7 @@ coq-interface (the same as coqtop).
 .BR coqc (1),
 .BR coqdep (1),
 .BR coqtop (1),
-.BR parser (1).
+.BR coq\-parser (1).
 .br
 .I
 The Coq Reference Manual.
diff --git a/man/coq-parser.1 b/man/coq-parser.1
new file mode 100644
index 00000000..23dc8201
--- /dev/null
+++ b/man/coq-parser.1
@@ -0,0 +1,30 @@
+.TH COQ 1 "April 25, 2001"
+
+.SH NAME
+coq\-parser \- Coq parser
+
+
+.SH SYNOPSIS
+.B coq\-parser
+[
+.B options
+]
+
+.SH DESCRIPTION
+
+.B parser
+is a program reading Coq proof developments and outputing them in the
+structured format given in the INRIA technical report RT154. This
+program is not for the casual user.
+
+.SH SEE ALSO
+
+.BR coq\-interface (1),
+.BR coqc (1),
+.BR coqtop (1),
+.BR coqdep (1).
+.br
+.I
+The Coq Reference Manual.
+.I
+The Coq web site: http://coq.inria.fr
diff --git a/man/coq-tex.1 b/man/coq-tex.1
index 737de70a..7e0a2f81 100644
--- a/man/coq-tex.1
+++ b/man/coq-tex.1
@@ -15,19 +15,19 @@ coq-tex \- Process Coq phrases embedded in LaTeX files
 .BI \-image \ coq-image
 ]
 [
-.B -w
+.B \-w
 ]
 [
-.B -v
+.B \-v
 ]
 [
-.B -sl
+.B \-sl
 ]
 [
-.B -hrule
+.B \-hrule
 ]
 [
-.B -small
+.B \-small
 ]
 .I input-file ...
 
@@ -75,7 +75,7 @@ typewriter font.
 .TP
 .BI \-o \ output-file
 Specify the name of a file where the LaTeX output is to be stored. A
-dash `-' causes the LaTeX output to be printed on standard output.
+dash `\-' causes the LaTeX output to be printed on standard output.
 .TP
 .BI \-n \ line-width
 Set the line width. The default is 72 characters. The responses of the
@@ -90,23 +90,23 @@ this is the command
 .IR coqtop
 without specifying any path which is used to evaluate the Coq phrases.
 .TP
-.B -w
+.B \-w
 Cause lines to be folded on a space character whenever possible,
 avoiding word cuts in the output. By default, folding occurs at
 the line width, regardless of word cuts.
 .TP
-.B -v
+.B \-v
 Verbose mode. Prints the Coq answers on the standard output.
 Useful to detect errors in Coq phrases.
 .TP
-.B -sl
+.B \-sl
 Slanted mode. The Coq answers are written in a slanted font.
 .TP
-.B -hrule
+.B \-hrule
 Horizontal lines mode. The Coq parts are written between two
 horizontal lines.
 .TP
-.B -small
+.B \-small
 Small font mode. The Coq parts are written in a smaller font.
 
 
diff --git a/man/coqdep.1 b/man/coqdep.1
index 6ae89f8b..e2cbb40e 100644
--- a/man/coqdep.1
+++ b/man/coqdep.1
@@ -67,7 +67,7 @@ Prints a warning if a Coq command
 .IR Module \&
 is incorrect. (For instance, you wrote `Declare ML Module "A".',
 but the module A contains #open "B"). The correct command is printed
-(see option -D). The warning is printed on standard error.
+(see option \-D). The warning is printed on standard error.
 .TP
 .BI \-i
 Prints also the dependencies for .vi files (Coq specification modules).
@@ -138,7 +138,7 @@ Z.v contains the commands `Require X' and `Declare ML Module "D"'.
 To get the dependencies of the Coq files:
 .IP
 .B
-example% coqdep -I . *.v
+example% coqdep \-I . *.v
 .RS
 .sp .5
 .nf
@@ -153,7 +153,7 @@ example% coqdep -I . *.v
 With a warning:
 .IP
 .B
-example% coqdep -w -I . *.v
+example% coqdep \-w \-I . *.v
 .RS
 .sp .5
 .nf
@@ -170,7 +170,7 @@ example% coqdep -w -I . *.v
 To get only the Caml dependencies:
 .IP
 .B
-example% coqdep -c -I . *.ml
+example% coqdep \-c \-I . *.ml
 .RS
 .sp .5
 .nf
@@ -190,4 +190,4 @@ example% coqdep -c -I . *.ml
 .SH BUGS
 
 Please report any bug to
-.B coq-bugs@pauillac.inria.fr
+.B coq\-bugs@pauillac.inria.fr
diff --git a/man/coqdoc.1 b/man/coqdoc.1
index c443e8b0..45fcafd2 100644
--- a/man/coqdoc.1
+++ b/man/coqdoc.1
@@ -54,7 +54,7 @@ Redirect the output into the file
 Output files into directory 
 .I dir 
 instead of current directory (option
--d does not change the filename specified with option -o, if any).
+\-d does not change the filename specified with option \-o, if any).
 .TP
 .B \-s, \ \-\-short
 Do not insert titles for the files. The default behavior is to insert
@@ -68,7 +68,7 @@ Suppress the header and trailer of the final document. Thus, you can
 insert the resulting document into a larger one.
 .TP
 .BI \-p \ string, \ \-\-preamble \ string
-Insert some material in the LATEX preamble, right before \\begin{document} (meaningless with -html).
+Insert some material in the LATEX preamble, right before \\begin{document} (meaningless with \-html).
 .TP
 .BI \-\-vernac\-file \ file, \ \-\-tex\-file \ file
 Considers the file `file' respectively as a .v (or .g) file or a .tex file.
@@ -114,7 +114,7 @@ it builds a table of contents into toc.html.
 .TP
 .B \-\-glob\-from \ file
 Make references using Coq globalizations from file file. (Such
-globalizations are obtained with Coq option -dump-glob).
+globalizations are obtained with Coq option \-dump\-glob).
 
 .TP
 .B \-\-no\-externals
@@ -129,22 +129,22 @@ Set base URL for the Coq standard library (default is http://coq.inria.fr/librar
 Set the base path where the Coq files are installed, especially style files coqdoc.sty and coqdoc.css.
 
 .TP
-.BI -R \ dir \  coqdir
+.BI \-R \ dir \  coqdir
 Map physical directory dir to Coq logical directory coqdir (similarly
-to Coq option -R).
+to Coq option \-R).
 .B Note: 
-option -R only has effect on the files following it on the command
+option \-R only has effect on the files following it on the command
 line, so you will probably need to put this option first.
 
 .SS Contents options
 
 .TP
-.B -g, \ --gallina
+.B \-g, \ \-\-gallina
 Do not print proofs.
 
 .TP
-.B -l, \ --light
-Light mode. Suppress proofs (as with -g) and the following commands:
+.B \-l, \ \-\-light
+Light mode. Suppress proofs (as with \-g) and the following commands:
 
         * [Recursive] Tactic Definition
         * Hint / Hints
@@ -153,29 +153,29 @@ Light mode. Suppress proofs (as with -g) and the following commands:
         * Implicit Argument / Implicits
         * Section / Variable / Hypothesis / End 
 
-The behavior of options -g and -l can be locally overridden using the (* begin show *) ... (* end show *) environment (see above).
+The behavior of options \-g and \-l can be locally overridden using the (* begin show *) ... (* end show *) environment (see above).
 
 .SS Language options
  
 Default behavior is to assume ASCII 7 bits input files.
 
 .TP 
-.B -latin1, \ --latin1
-Select ISO-8859-1 input files. It is equivalent to --inputenc latin1
---charset iso-8859-1.
+.B \-latin1, \ \-\-latin1
+Select ISO-8859-1 input files. It is equivalent to \-\-inputenc latin1
+\-\-charset iso\-8859\-1.
 
 .TP 
-.B -utf8, \ --utf8
-Select UTF-8 (Unicode) input files. It is equivalent to --inputenc
-utf8 --charset utf-8. LATEX UTF-8 support can be found at
-http://www.ctan.org/tex-archive/macros/latex/contrib/supported/unicode/.
+.B \-utf8, \ \-\-utf8
+Select UTF-8 (Unicode) input files. It is equivalent to \-\-inputenc
+utf8 \-\-charset utf\-8. LATEX UTF-8 support can be found at
+http://www.ctan.org/tex\-archive/macros/latex/contrib/supported/unicode/.
 
 .TP 
-.BI --inputenc \ string
+.BI \-\-inputenc \ string
 Give a LATEX input encoding, as an option to LATEX package inputenc.
 
 .TP
-.BI --charset \ string
+.BI \-\-charset \ string
 Specify the HTML character set, to be inserted in the HTML header.
 
 
diff --git a/man/coqide.1 b/man/coqide.1
new file mode 100644
index 00000000..20379ef4
--- /dev/null
+++ b/man/coqide.1
@@ -0,0 +1,166 @@
+.TH COQIDE 1 "July 16, 2004"
+
+.SH NAME
+coqide \- The Coq Proof Assistant graphical interface
+
+
+.SH SYNOPSIS
+.B coqide
+[
+.B options
+]
+
+.SH DESCRIPTION
+
+.B coqtop
+is a gtk graphical interface for the Coq proof assistant.
+
+For command-line-oriented use of Coq, see
+.BR coqide (1)
+; for batch-oriented use of Coq, see 
+.BR coqc (1).
+
+
+.SH OPTIONS
+
+.TP
+.B \-h
+Show the complete list of options accepted by
+.BR coqide .
+.TP
+.BI \-I\  dir ,\ \-include\  dir
+Add directory dir in the include path.
+.TP
+.BI \-R\  dir\ coqdir
+Recursively map physical
+.I dir
+to logical
+.IR coqdir .
+.TP
+.B \-src
+Add source directories in the include path.
+.TP
+.BI \-is\  f ,\ \-inputstate\  f
+Read state from
+.IR f .coq.
+.TP
+.B \-nois
+Start with an empty state.
+.TP
+.BI \-outputstate\  f
+Write state in file
+.IR f .coq.
+.TP
+.BI \-load\-ml\-object\  f
+Load ML object file
+.IR f .
+.TP
+.BI \-load\-ml\-source\  f
+Load ML file
+.IR f .
+.TP
+.BI \-l\  f ,\ \-load\-vernac\-source\  f
+Load Coq file
+.IR f .v
+(Load
+.IR f .).
+.TP
+.BI \-lv\  f ,\ \-load\-vernac\-source\-verbose\  f
+Load Coq file
+.IR f .v
+(Load Verbose
+.IR f .).
+.TP
+.BI \-load\-vernac\-object\  f
+Load Coq object file
+.IR f .vo.
+.TP
+.BI \-require\  f
+Load Coq object file
+.IR f .vo
+and import it (Require
+.IR f .).
+.TP
+.BI \-compile\  f
+Compile Coq file
+.IR f .v
+(implies
+.BR \-batch ).
+.TP
+.BI \-compile\-verbose\  f
+Verbosely compile Coq file
+.IR f .v
+(implies
+.BR -batch ).
+.TP
+.B \-opt
+Run the native-code version of Coq or Coq_SearchIsos.
+.TP
+.B \-byte
+Run the bytecode version of Coq or Coq_SearchIsos.
+.TP
+.B \-where
+Print Coq's standard library location and exit.
+.TP
+.B -v
+Print Coq version and exit.
+.TP
+.B \-q
+Skip loading of rcfile.
+.TP
+.BI \-init\-file\  f
+Set the rcfile to
+.IR f .
+.TP
+.BI \-user\  u
+Use the rcfile of user
+.IR u .
+.TP
+.B \-batch
+Batch mode (exits just after arguments parsing).
+.TP
+.B \-boot
+Boot mode (implies
+.B \-q
+and
+.BR \-batch ).
+.TP
+.B \-emacs
+Tells Coq it is executed under Emacs.
+.TP
+.BI \-dump\-glob\  f
+Dump globalizations in file
+.I f
+(to be used by
+.BR coqdoc (1)).
+.TP
+.B \-impredicative\-set
+Set sort Set impredicative.
+.TP
+.B \-dont\-load\-proofs
+Don't load opaque proofs in memory.
+.TP
+.B \-xml
+Export XML files either to the hierarchy rooted in
+the directory
+.B COQ_XML_LIBRARY_ROOT
+(if set) or to stdout (if unset).
+
+
+.SH SEE ALSO
+
+.BR coqc (1),
+.BR coqtop (1),
+.BR coq-tex (1),
+.BR coqdep (1).
+.br
+.I
+The Coq Reference Manual,
+.I
+The Coq web site: http://coq.inria.fr,
+.I
+/usr/share/doc/coqide/FAQ.
+
+.SH AUTHOR
+This manual page was written by Samuel Mimram <samuel.mimram@ens-lyon.org>,
+for the Debian project (but may be used by others).
diff --git a/man/coqmktop.1 b/man/coqmktop.1
index 3640d439..1b9c9e2a 100644
--- a/man/coqmktop.1
+++ b/man/coqmktop.1
@@ -17,10 +17,10 @@ coqmktop \- The Coq Proof Assistant user-tactics linker
 .B coqmktop
 builds a new Coq toplevel extended with user-tactics.
 .IR files \&
-are the Objective Caml object or library files (i.e. with suffix .cmo,
-.cmx, .cma or .cmxa) to link with the Coq system.
+are the Objective Caml object or library files
+(i.e. with suffix .cmo, .cmx, .cma or .cmxa) to link with the Coq system.
 The linker produces an executable Coq toplevel which can be called
-directly or through coqc(1), using the -image option.
+directly or through coqc(1), using the \-image option.
 
 .SH OPTIONS
 
diff --git a/man/coqwc.1 b/man/coqwc.1
index 7011d148..4594aeec 100644
--- a/man/coqwc.1
+++ b/man/coqwc.1
@@ -44,4 +44,4 @@ Do not skip headers
 .SH BUGS
 
 Please report any bug to
-.B coq-bugs@pauillac.inria.fr
+.B coq\-bugs@pauillac.inria.fr
diff --git a/man/parser.1 b/man/parser.1
deleted file mode 100644
index d89465d8..00000000
--- a/man/parser.1
+++ /dev/null
@@ -1,30 +0,0 @@
-.TH COQ 1 "April 25, 2001"
-
-.SH NAME
-parser \- Coq parser
-
-
-.SH SYNOPSIS
-.B parser
-[
-.B options
-]
-
-.SH DESCRIPTION
-
-.B parser
-is a program reading Coq proof developments and outputing them in the
-structured format given in the INRIA technical report RT154. This
-program is not for the casual user.
-
-.SH SEE ALSO
-
-.BR coq-interface (1),
-.BR coqc (1),
-.BR coqtop (1),
-.BR coqdep (1).
-.br
-.I
-The Coq Reference Manual.
-.I
-The Coq web site: http://coq.inria.fr
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 3aa51c53..4811c443 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -10,7 +10,7 @@
  * on May-June 2006 for implementation of abstraction of pretty-printing of objects.
  *)
 
-(* $Id: prettyp.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: prettyp.ml 11343 2008-09-01 20:55:13Z herbelin $ *)
 
 open Pp
 open Util
@@ -744,7 +744,7 @@ let print_path_between cls clt =
   let j = index_of_class clt in
   let p = 
     try 
-      lookup_path_between (i,j) 
+      lookup_path_between_class (i,j) 
     with _ -> 
       errorlabstrm "index_cl_of_id"
         (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt
diff --git a/parsing/printmod.ml b/parsing/printmod.ml
index 0bdae7c7..be73f573 100644
--- a/parsing/printmod.ml
+++ b/parsing/printmod.ml
@@ -60,10 +60,10 @@ let rec print_module name locals with_body mb =
   in
   let modtype = match mb.mod_type with
       None -> str ""
-    | Some t ->  str": " ++ 
+    | Some t -> spc () ++ str": " ++ 
 	print_modtype locals t
   in
-    hv 2 (str "Module " ++ name ++ spc () ++ modtype ++ body)
+    hv 2 (str "Module " ++ name ++ modtype ++ body)
 
 and print_modtype locals mty = 
   match mty with
@@ -102,7 +102,7 @@ and print_sig locals msid sign =
     | SFBconst {const_opaque=true} -> str "Parameter "
     | SFBmind _ -> str "Inductive "
     | SFBmodule _ -> str "Module "
-    | SFBalias (mp,_) -> str "Module"
+    | SFBalias (mp,_) -> str "Module "
     | SFBmodtype _ -> str "Module Type ") ++ str (string_of_label l)
   in
     prlist_with_sep spc print_spec sign
@@ -114,7 +114,7 @@ and print_struct locals msid struc =
     | SFBconst {const_body=None} -> str "Parameter "
     | SFBmind _ -> str "Inductive "
     | SFBmodule _ -> str "Module "
-    | SFBalias (mp,_) -> str "Module"
+    | SFBalias (mp,_) -> str "Module "
     | SFBmodtype _ -> str "Module Type ") ++ str (string_of_label l)
   in
     prlist_with_sep spc print_body struc
@@ -125,9 +125,9 @@ and print_modexpr locals mexpr = match mexpr with
 (*    let env' = Modops.add_module (MPbid mbid) (Modops.body_of_type mtb) env 
       in *)
       let locals' = (mbid, get_new_id locals (id_of_mbid mbid))::locals in
-      hov 2 (str "Functor" ++ spc() ++ str"[" ++ pr_id(id_of_mbid mbid) ++ 
+      hov 2 (str "Functor" ++ spc() ++ str"(" ++ pr_id(id_of_mbid mbid) ++ 
 	     str ":" ++ print_modtype locals mty.typ_expr ++ 
-      str "]" ++ spc () ++ print_modexpr locals' mexpr)
+      str ")" ++ spc () ++ print_modexpr locals' mexpr)
   | SEBstruct (msid, struc) -> 
       hv 2 (str "Struct" ++ spc () ++ print_struct locals msid struc ++ brk (1,-2) ++ str "End")
   | SEBapply (mexpr,marg,_) -> 
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index b5a5709e..398da529 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: classops.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: classops.ml 11343 2008-09-01 20:55:13Z herbelin $ *)
 
 open Util
 open Pp
@@ -128,6 +128,10 @@ let class_exists cl = Bijint.mem cl !class_tab
 
 let class_info_from_index i = Bijint.map i !class_tab
 
+let cl_fun_index = fst(class_info CL_FUN)
+
+let cl_sort_index = fst(class_info CL_SORT)
+
 (* coercion_info : coe_typ -> coe_info_typ *)
 
 let coercion_info coe = Gmap.find coe !coercion_tab
@@ -136,32 +140,10 @@ let coercion_exists coe = Gmap.mem coe !coercion_tab
 
 let coercion_params coe_info = coe_info.coe_param
 
-let lookup_path_between (s,t) =
-  Gmap.find (s,t) !inheritance_graph
-
-let lookup_path_to_fun_from s = 
-  lookup_path_between (s,fst(class_info CL_FUN))
+(* find_class_type : env -> evar_map -> constr -> cl_typ * int *)
 
-let lookup_path_to_sort_from s = 
-  lookup_path_between (s,fst(class_info CL_SORT))
-
-let lookup_pattern_path_between (s,t) =
-  let l = Gmap.find (s,t) !inheritance_graph in
-  List.map  
-    (fun coe ->
-       let c, _ =
-	 Reductionops.whd_betadeltaiota_stack (Global.env()) Evd.empty 
-	   coe.coe_value
-       in 
-       match kind_of_term c with
-	 | Construct cstr ->
-	     (cstr, Inductiveops.constructor_nrealargs (Global.env()) cstr -1)
-	 | _ -> raise Not_found) l
-
-(* find_class_type : constr -> cl_typ * int *)
-
-let find_class_type t =
-  let t', args = decompose_app (Reductionops.whd_betaiotazeta t) in
+let find_class_type env sigma t =
+  let t', args = Reductionops.whd_betaiotazetaevar_stack env sigma t in
   match kind_of_term t' with
     | Var id -> CL_SECVAR id, args
     | Const sp -> CL_CONST sp, args
@@ -178,7 +160,7 @@ let subst_cl_typ subst ct = match ct with
   | CL_CONST kn -> 
       let kn',t = subst_con subst kn in 
 	if kn' == kn then ct else
-         fst (find_class_type t)
+         fst (find_class_type (Global.env()) Evd.empty t)
   | CL_IND (kn,i) ->
       let kn' = subst_kn subst kn in 
 	if kn' == kn then ct else
@@ -188,19 +170,17 @@ let subst_cl_typ subst ct = match ct with
        to declare any term as a coercion *)
 let subst_coe_typ subst t = fst (subst_global subst t)
 
-(* classe d'un terme *)
-
 (* class_of : Term.constr -> int *)
 
 let class_of env sigma t = 
   let (t, n1, i, args) = 
     try
-      let (cl,args) = find_class_type t in
+      let (cl,args) = find_class_type env sigma t in
       let (i, { cl_param = n1 } ) = class_info cl in
       (t, n1, i, args)
     with Not_found ->
       let t = Tacred.hnf_constr env sigma t in
-      let (cl, args) = find_class_type t in 
+      let (cl, args) = find_class_type env sigma t in 
       let (i, { cl_param = n1 } ) = class_info cl in
       (t, n1, i, args)
   in
@@ -208,7 +188,7 @@ let class_of env sigma t =
 
 let inductive_class_of ind = fst (class_info (CL_IND ind))
 
-let class_args_of c = snd (find_class_type c)
+let class_args_of env sigma c = snd (find_class_type env sigma c)
 
 let string_of_class = function
   | CL_FUN -> "Funclass"
@@ -222,6 +202,61 @@ let string_of_class = function
 
 let pr_class x = str (string_of_class x)
 
+(* lookup paths *)
+
+let lookup_path_between_class (s,t) =
+  Gmap.find (s,t) !inheritance_graph
+
+let lookup_path_to_fun_from_class s =
+  lookup_path_between_class (s,cl_fun_index)
+
+let lookup_path_to_sort_from_class s =
+  lookup_path_between_class (s,cl_sort_index)
+
+(* advanced path lookup *)
+
+let apply_on_class_of env sigma t cont =
+  try
+    let (cl,args) = find_class_type env sigma t in
+    let (i, { cl_param = n1 } ) = class_info cl in
+    if List.length args <> n1 then raise Not_found;
+    t, cont i
+  with Not_found ->
+    (* Is it worth to be more incremental on the delta steps? *)
+    let t = Tacred.hnf_constr env sigma t in
+    let (cl, args) = find_class_type env sigma t in 
+    let (i, { cl_param = n1 } ) = class_info cl in
+    if List.length args <> n1 then raise Not_found;
+    t, cont i
+
+let lookup_path_between env sigma (s,t) =
+  let (s,(t,p)) =
+    apply_on_class_of env sigma s (fun i ->
+      apply_on_class_of env sigma t (fun j ->
+	lookup_path_between_class (i,j))) in
+  (s,t,p)
+
+let lookup_path_to_fun_from env sigma s =
+  apply_on_class_of env sigma s lookup_path_to_fun_from_class
+
+let lookup_path_to_sort_from env sigma s = 
+  apply_on_class_of env sigma s lookup_path_to_sort_from_class
+
+let get_coercion_constructor coe =
+  let c, _ =
+    Reductionops.whd_betadeltaiota_stack (Global.env()) Evd.empty coe.coe_value
+  in
+  match kind_of_term c with
+  | Construct cstr -> 
+      (cstr, Inductiveops.constructor_nrealargs (Global.env()) cstr -1)
+  | _ ->
+      raise Not_found
+
+let lookup_pattern_path_between (s,t) =
+  let i = inductive_class_of s in
+  let j = inductive_class_of t in
+  List.map get_coercion_constructor (Gmap.find (i,j) !inheritance_graph)
+
 (* coercion_value : coe_index -> unsafe_judgment * bool *)
 
 let coercion_value { coe_value = c; coe_type = t; coe_is_identity = b } =
@@ -255,11 +290,11 @@ let add_coercion_in_graph (ic,source,target) =
     try 
       if i=j then begin
 	if different_class_params i j then begin
-	  let _ = lookup_path_between ij in
+	  let _ = lookup_path_between_class ij in
           ambig_paths := (ij,p)::!ambig_paths
 	end
       end else begin
-        let _ = lookup_path_between (i,j) in
+        let _ = lookup_path_between_class (i,j) in
         ambig_paths := (ij,p)::!ambig_paths
       end;
       false
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 1436a11b..a76fe75c 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: classops.mli 10840 2008-04-23 21:29:34Z herbelin $ i*)
+(*i $Id: classops.mli 11343 2008-09-01 20:55:13Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -52,17 +52,17 @@ val class_info : cl_typ -> (cl_index * cl_info_typ)
 val class_exists : cl_typ -> bool
 val class_info_from_index : cl_index -> cl_typ * cl_info_typ
 
-(* [find_class_type c] returns the head reference of c and its
+(* [find_class_type env sigma c] returns the head reference of [c] and its
    arguments *)
-val find_class_type : constr -> cl_typ * constr list
+val find_class_type : env -> evar_map -> types -> cl_typ * constr list
 
 (* raises [Not_found] if not convertible to a class *)
-val class_of : env -> evar_map -> constr -> constr * cl_index
+val class_of : env -> evar_map -> types -> types * cl_index
 
 (* raises [Not_found] if not mapped to a class *)
 val inductive_class_of : inductive -> cl_index
 
-val class_args_of : constr -> constr list
+val class_args_of : env -> evar_map -> types -> constr list
 
 (*s [declare_coercion] adds a coercion in the graph of coercion paths *)
 val declare_coercion : 
@@ -75,11 +75,16 @@ val coercion_exists : coe_typ -> bool
 val coercion_value : coe_index -> (unsafe_judgment * bool)
 
 (*s Lookup functions for coercion paths *)
-val lookup_path_between : cl_index * cl_index -> inheritance_path
-val lookup_path_to_fun_from : cl_index -> inheritance_path
-val lookup_path_to_sort_from : cl_index -> inheritance_path
-val lookup_pattern_path_between :
-  cl_index * cl_index -> (constructor * int) list
+val lookup_path_between_class : cl_index * cl_index -> inheritance_path
+
+val lookup_path_between : env -> evar_map -> types * types -> 
+      types * types * inheritance_path
+val lookup_path_to_fun_from : env -> evar_map -> types ->
+      types * inheritance_path
+val lookup_path_to_sort_from : env -> evar_map -> types -> 
+      types * inheritance_path
+val lookup_pattern_path_between : 
+  inductive * inductive -> (constructor * int) list
 
 (*i Crade *)
 open Pp
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 3074c4c4..73fcd0ea 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -5,7 +5,7 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(* $Id: coercion.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
+(* $Id: coercion.ml 11343 2008-09-01 20:55:13Z herbelin $ *)
 
 open Util
 open Names
@@ -78,10 +78,6 @@ module Default = struct
       | App (f,l) -> mkApp (whd_evar sigma f,l)
       | _ -> whd_evar sigma t
 
-  let class_of1 env evd t =
-    let sigma = evars_of evd in
-    class_of env sigma (whd_app_evar sigma t)
-
   (* Here, funj is a coercion therefore already typed in global context *)
   let apply_coercion_args env argl funj =
     let rec apply_rec acc typ = function
@@ -107,18 +103,16 @@ module Default = struct
 
   (* raise Not_found if no coercion found *)
   let inh_pattern_coerce_to loc pat ind1 ind2 =
-    let i1 = inductive_class_of ind1 in
-    let i2 = inductive_class_of ind2 in
-    let p = lookup_pattern_path_between (i1,i2) in
+    let p = lookup_pattern_path_between (ind1,ind2) in
       apply_pattern_coercion loc pat p
 
   (* appliquer le chemin de coercions p à hj *)
-  let apply_coercion env p hj typ_cl =
+  let apply_coercion env sigma p hj typ_cl =
     try 
       fst (List.fold_left
              (fun (ja,typ_cl) i -> 
 		let fv,isid = coercion_value i in
-		let argl = (class_args_of typ_cl)@[ja.uj_val] in
+		let argl = (class_args_of env sigma typ_cl)@[ja.uj_val] in
 		let jres = apply_coercion_args env argl fv in
 		  (if isid then 
 		     { uj_val = ja.uj_val; uj_type = jres.uj_type }
@@ -137,16 +131,15 @@ module Default = struct
 	      (evd',{ uj_val = j.uj_val; uj_type = t })
 	| _ ->
        	    (try
- 	       let t,i1 = class_of1 env evd j.uj_type in
-      	       let p = lookup_path_to_fun_from i1 in
-		 (evd,apply_coercion env p j t)
+      	       let t,p =
+		 lookup_path_to_fun_from env (evars_of evd) j.uj_type in
+		 (evd,apply_coercion env (evars_of evd) p j t)
 	     with Not_found -> (evd,j))
 
   let inh_tosort_force loc env evd j =
     try
-      let t,i1 = class_of1 env evd j.uj_type in
-      let p = lookup_path_to_sort_from i1 in
-      let j1 = apply_coercion env p j t in 
+      let t,p = lookup_path_to_sort_from env (evars_of evd) j.uj_type in
+      let j1 = apply_coercion env (evars_of evd) p j t in 
       let j2 = on_judgment_type (whd_evar (evars_of evd)) j1 in
         (evd,type_judgment env j2)
     with Not_found ->
@@ -173,12 +166,12 @@ module Default = struct
     else
     let v', t' =
       try 
-	let t1,i1 = class_of1 env evd c1 in
-	let t2,i2 = class_of1 env evd t in
-	let p = lookup_path_between (i2,i1) in
+	let t2,t1,p = lookup_path_between env (evars_of evd) (t,c1) in
 	  match v with
 	      Some v -> 
-		let j = apply_coercion env p {uj_val = v; uj_type = t} t2 in
+		let j =
+		  apply_coercion env (evars_of evd) p
+		    {uj_val = v; uj_type = t} t2 in
 		  Some j.uj_val, j.uj_type
 	    | None -> None, t
       with Not_found -> raise NoCoercion 
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 2f507318..21e881b9 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: reductionops.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: reductionops.ml 11343 2008-09-01 20:55:13Z herbelin $ *)
 
 open Pp
 open Util
@@ -233,6 +233,7 @@ let evar = mkflags [fevar]
 let betaevar = mkflags [fevar; fbeta]
 let betaiota = mkflags [fiota; fbeta]
 let betaiotazeta = mkflags [fiota; fbeta;fzeta]
+let betaiotazetaevar = mkflags [fiota; fbeta;fzeta;fevar]
 
 (* Contextual *)
 let delta = mkflags [fdelta;fevar]
@@ -483,6 +484,12 @@ let whd_betaiotazeta_stack x =
 let whd_betaiotazeta x =
   app_stack (whd_betaiotazeta_state (x, empty_stack))
 
+let whd_betaiotazetaevar_state = whd_state_gen betaiotazetaevar
+let whd_betaiotazetaevar_stack env sigma x =
+  appterm_of_stack (whd_betaiotazetaevar_state env sigma (x, empty_stack))
+let whd_betaiotazetaevar env sigma x =
+  app_stack (whd_betaiotazetaevar_state env sigma (x, empty_stack))
+
 let whd_betaiotaevar_state e = whd_state_gen betaiotaevar e
 let whd_betaiotaevar_stack env sigma x =
   appterm_of_stack (whd_betaiotaevar_state env sigma (x, empty_stack))
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 1ac36b2a..c026d9fe 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: reductionops.mli 11309 2008-08-06 10:30:35Z herbelin $ i*)
+(*i $Id: reductionops.mli 11343 2008-09-01 20:55:13Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -98,6 +98,7 @@ val whd_evar :  evar_map -> constr -> constr
 val whd_beta : local_reduction_function
 val whd_betaiota : local_reduction_function
 val whd_betaiotazeta : local_reduction_function
+val whd_betaiotazetaevar : contextual_reduction_function
 val whd_betadeltaiota :  contextual_reduction_function
 val whd_betadeltaiota_nolet :  contextual_reduction_function
 val whd_betaetalet : local_reduction_function
@@ -105,17 +106,17 @@ val whd_betalet : local_reduction_function
 
 val whd_beta_stack : local_stack_reduction_function
 val whd_betaiota_stack : local_stack_reduction_function
-val whd_betaiotazeta_stack : local_stack_reduction_function
-val whd_betadeltaiota_stack :  contextual_stack_reduction_function
-val whd_betadeltaiota_nolet_stack :  contextual_stack_reduction_function
+val whd_betaiotazetaevar_stack : contextual_stack_reduction_function
+val whd_betadeltaiota_stack : contextual_stack_reduction_function
+val whd_betadeltaiota_nolet_stack : contextual_stack_reduction_function
 val whd_betaetalet_stack : local_stack_reduction_function
 val whd_betalet_stack : local_stack_reduction_function
 
 val whd_beta_state : local_state_reduction_function
 val whd_betaiota_state : local_state_reduction_function
-val whd_betaiotazeta_state : local_state_reduction_function
-val whd_betadeltaiota_state :  contextual_state_reduction_function
-val whd_betadeltaiota_nolet_state :  contextual_state_reduction_function
+val whd_betaiotazetaevar_state : contextual_state_reduction_function
+val whd_betadeltaiota_state : contextual_state_reduction_function
+val whd_betadeltaiota_nolet_state : contextual_state_reduction_function
 val whd_betaetalet_state : local_state_reduction_function
 val whd_betalet_state : local_state_reduction_function
 
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index e87a195f..2569b292 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqmktop.ml 11260 2008-07-24 20:53:12Z letouzey $ *)
+(* $Id: coqmktop.ml 11380 2008-09-07 12:27:27Z glondu $ *)
 
 (* coqmktop is a script to link Coq, analogous to ocamlmktop.
    The command line contains options specific to coqmktop, options for the
@@ -289,7 +289,8 @@ let main () =
       (* bytecode (we shunt ocamlmktop script which fails on win32) *)
       let ocamlmktoplib = " toplevellib.cma" in
       let ocamlcexec = Filename.concat Coq_config.camldir "ocamlc" in
-      let ocamlccustom = ocamlcexec^" -custom -linkall" in
+      let ocamlccustom = Printf.sprintf "%s %s -linkall "
+        ocamlcexec Coq_config.coqrunbyteflags in
       (if !top then ocamlccustom^ocamlmktoplib else ocamlccustom)
   in
   (* files to link *)
diff --git a/test-suite/check b/test-suite/check
index 571e7a67..47960e98 100755
--- a/test-suite/check
+++ b/test-suite/check
@@ -65,7 +65,7 @@ test_output() {
     done
 }
 
-# La fonction suivante teste l'analyseur syntaxique fournit par "parser"
+# La fonction suivante teste l'analyseur syntaxique fournit par "coq-parser"
 # Elle fonctionne comme test_output
 test_parser() {
     if [ -d $1 ]; then
@@ -74,7 +74,7 @@ test_parser() {
         printf "    "$f"..."
         tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`
         foutput=`dirname $f`/`basename $f .v`.out
-        echo "parse_file 1 \"$f\"" | ../bin/parser > $tmpoutput 2>&1
+        echo "parse_file 1 \"$f\"" | ../bin/coq-parser > $tmpoutput 2>&1
         perl -ne 'if(/Starting.*Parser Loop/){$printit = 1};print if $printit' \
             $tmpoutput 2>&1 | grep -i error > /dev/null
         if [ $? = 0 ] ; then
@@ -250,8 +250,16 @@ echo "Interactive tests"
 test_interactive interactive
 echo "Micromega tests"
 test_success micromega
-echo "Complexity tests"
-test_complexity complexity
+
+# We give a chance to disable the complexity tests which may cause
+# random build failures on build farms
+if [ -z "$COQTEST_SKIPCOMPLEXITY" ]; then
+  echo "Complexity tests"
+  test_complexity complexity
+else
+  echo "Skipping complexity tests"
+fi
+
 echo "Module tests"
 $coqtop -compile modules/Nat
 $coqtop -compile modules/plik
diff --git a/test-suite/success/coercions.v b/test-suite/success/coercions.v
index d652132e..525348de 100644
--- a/test-suite/success/coercions.v
+++ b/test-suite/success/coercions.v
@@ -61,3 +61,24 @@ Check fun (H : For_all (fun x => C (f x))) => H : For_all (fun x => D (f x)).
 
 End Q.
 
+(* Combining class lookup and path lookup so that if a lookup fails, another
+   descent in the class can be found (see wish #1934) *)
+
+Record Setoid : Type :=
+{ car :>  Type }.
+
+Record Morphism (X Y:Setoid) : Type :=
+{evalMorphism :> X -> Y}.
+
+Definition extSetoid (X Y:Setoid) : Setoid.
+intros X Y.
+constructor.
+exact (Morphism X Y).
+Defined.
+
+Definition ClaimA := forall (X Y:Setoid) (f: extSetoid X Y) x, f x= f x.
+
+Coercion irrelevent := (fun _ => I) : True -> car (Build_Setoid True).
+
+Definition ClaimB := forall (X Y:Setoid) (f: extSetoid X Y) (x:X), f x= f x.
+
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 94444f5b..05cd1892 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id: FMapFacts.v 11282 2008-07-28 11:51:53Z msozeau $ *)
+(* $Id: FMapFacts.v 11359 2008-09-04 09:43:36Z notin $ *)
 
 (** * Finite maps library *)
 
@@ -975,7 +975,7 @@ Module WProperties (E:DecidableType)(M:WSfun E).
    fold (fun k e b => if f k e then true else b) m false.
 
   Definition partition (f : key -> elt -> bool)(m : t elt) := 
-   (filter f m, filter (fun k e => negb (f k e))).
+   (filter f m, filter (fun k e => negb (f k e)) m).
 
   Section Specs.
   Variable f : key -> elt -> bool.
diff --git a/tools/coqdoc/coqdoc.css b/tools/coqdoc/coqdoc.css
index 3900987e..65c39b7a 100644
--- a/tools/coqdoc/coqdoc.css
+++ b/tools/coqdoc/coqdoc.css
@@ -24,7 +24,8 @@ body { padding: 0px 0px;
 #main{ display: block;
        padding: 10px;
        overflow: hidden;
-       font-size: 10pt }
+       font-size: 100%;
+       line-height: 80% }
 
 #main  a.idref:visited {color : #416DFF; text-decoration : none; }
 #main  a.idref:link {color : #416DFF; text-decoration : none; }
@@ -39,16 +40,16 @@ body { padding: 0px 0px;
 #main .keyword { color : #cf1d1d }
 #main { color: black }
 
-#main .section { background-color:#899BD6;
-                 font-size : 20pt }
+#main .section { background-color:#90bdff;
+                 font-size : 175% }
 
-#main code { font-family: monospace; 
-             line-height: 50% }
+#main code { font-family: monospace }
 
 #main .doc { margin: 0px;
              padding: 10px;
              font-family: sans-serif;
-             font-size: 11pt;
+             font-size: 100%;
+	     line-height: 100%;
              font-weight:bold;
              color: black;
              background-color: #90bdff;
@@ -58,7 +59,7 @@ body { padding: 0px 0px;
 
 /* Pied de page */
 
-#footer { font-size: 8pt;
+#footer { font-size: 65%;
           font-family: sans-serif; }
 
 #footer a:visited { color: blue; }
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 2c6a63b0..6ebc663b 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: class.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: class.ml 11343 2008-09-01 20:55:13Z herbelin $ *)
 
 open Util
 open Pp
@@ -139,7 +139,7 @@ let get_source lp source =
 	let (cl1,lv1) =
           match lp with
 	    | [] -> raise Not_found
-            | t1::_ -> find_class_type t1
+            | t1::_ -> find_class_type (Global.env()) Evd.empty t1
         in 
 	(cl1,lv1,1)
     | Some cl ->
@@ -147,7 +147,7 @@ let get_source lp source =
 	  | [] -> raise Not_found
 	  | t1::lt ->
 	      try 
-		let cl1,lv1 = find_class_type t1 in
+		let cl1,lv1 = find_class_type (Global.env()) Evd.empty t1 in
 		if cl = cl1 then cl1,lv1,(List.length lt+1)
 		else raise Not_found
               with Not_found -> aux lt
@@ -157,7 +157,7 @@ let get_target t ind =
   if (ind > 1) then 
     CL_FUN
   else 
-    fst (find_class_type t)
+    fst (find_class_type (Global.env()) Evd.empty t)
 
 let prods_of t = 
   let rec aux acc d = match kind_of_term d with
@@ -225,8 +225,9 @@ let build_id_coercion idf_opt source =
     match idf_opt with
       | Some idf -> idf
       | None ->
+	  let cl,_ = find_class_type (Global.env()) Evd.empty t in
 	  id_of_string ("Id_"^(ident_key_of_class source)^"_"^
-                        (ident_key_of_class (fst (find_class_type t)))) 
+                        (ident_key_of_class cl))
   in
   let constr_entry = (* Cast is necessary to express [val_f] is identity *)
     DefinitionEntry
-- 
cgit v1.2.3