Imported Upstream version 8.2-1+dfsgupstream/8.2-1+dfsg

72 files changed, 1143 insertions, 600 deletions

diff --git a/CHANGES b/CHANGES
index 035579cd..494575fa 100644
--- a/CHANGES
+++ b/CHANGES
@@ -489,9 +489,10 @@ Miscellaneous
   "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.
-- 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.
+- Build a shared library for the C part of Coq, and use it by default on
+  non-(Windows or MacOS) systems. Bytecode executables are now pure. The
+  behaviour is configurable with -coqrunbyteflags, -coqtoolsbyteflags and
+  -custom configure options.
 - Complexity tests can be skipped by setting the environment variable
   COQTEST_SKIPCOMPLEXITY.
 
diff --git a/INSTALL b/INSTALL
index 626417d6..47d2cb2e 100644
--- a/INSTALL
+++ b/INSTALL
@@ -71,10 +71,12 @@ WHAT DO YOU NEED ?
 
      - a C compiler
 
-     - for Coqide, the Lablgtk development files, and the GTK libraries, see INSTALL.ide for more details
+     - for Coqide, the Lablgtk development files, and the GTK
+       libraries, see INSTALL.ide for more details
 
-   By FTP, Coq comes as a single compressed tar-file. You have
-   probably already decompressed it if you are reading this document.
+   Coq sources distribution comes as a single compressed tar-file. You
+   have probably already decompressed it if you are reading this
+   document.
 
 
 QUICK INSTALLATION PROCEDURE.
@@ -99,21 +101,18 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
    bigger), you will also need the "ocamlopt" (or its native code version
    "ocamlopt.opt") command.
 
-2- Check that you have Camlp4 installed on your 
-   computer and that the command "camlp4" lies in a directory which
-   is present in your $PATH environment variable path.
-   (You need Camlp4 in both bytecode and native versions if
-   your platform supports it).
-
-   Note: in the latest ocaml distributions, camlp4 comes with ocaml so
-   you do not have to check this point anymore.
+2- If you are using OCaml version >= 3.10.0, check that you have
+   Camlp5 installed on your computer and that the command "camlp5"
+   lies in a directory which is present in your $PATH environment
+   variable path.  (You need Camlp5 in both bytecode and native
+   versions if your platform supports it).
 
 3- The uncompression and un-tarring of the distribution file gave birth 
    to a directory named "coq-8.xx". You can rename this directory and put 
    it wherever you want. Just keep in mind that you will need some spare
-   space during the compilation (reckon on about 50 Mb of disk space
+   space during the compilation (reckon on about 250 Mb of disk space
    for the whole system in native-code compilation). Once installed, the
-   binaries take about 14 Mb, and the library about 9 Mb.
+   binaries take about 65 Mb, and the library about 60 Mb.
 
 4- First you need to configure the system. It is done automatically with
    the command:
@@ -313,12 +312,9 @@ MOVING BINARIES OR LIBRARY.
 	Error: Can't find file initial.coq on loadpath
 
    If you really have (or want) to move the binaries or the library, then
-   you have to indicate their new places to Coq, using the options -bindir (for
-   the binaries directory) and -libdir (for the standard library directory) :
-
-	coqtop -bindir <new directory> -libdir <new directory>
+   you have to indicate where Coq will find the libraries:
 
-   See also next section.
+	coqtop -coqlib <directory>
 
 
 DYNAMICALLY LOADED LIBRARIES FOR BYTECODE EXECUTABLES.
@@ -344,6 +340,6 @@ DYNAMICALLY LOADED LIBRARIES FOR BYTECODE EXECUTABLES.
        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 ...
+         ./configure -custom ...
        be aware that stripping executables generated this way, or performing
        other executable-specific operations, will make them useless.
diff --git a/INSTALL.macosx b/INSTALL.macosx
index 121a3e0b..fc33351a 100644
--- a/INSTALL.macosx
+++ b/INSTALL.macosx
@@ -16,5 +16,6 @@ team. To use the MacOS X package,:
    can be used from a Terminal window: the interactive toplevel is
    named coqtop and the compiler is coqc.
 
-If you have any trouble with this installation, please contact:
-coq-bugs@pauillac.inria.fr.
+If you have any trouble with this installation, please consider using
+our bug tracking system to report bug (see
+http://logical.saclay.inria.fr/coq-bugs).
diff --git a/KNOWN-BUGS b/KNOWN-BUGS
deleted file mode 100644
index 774d181c..00000000
--- a/KNOWN-BUGS
+++ /dev/null
@@ -1,20 +0,0 @@
-  THIS IS A LIST OF KNOWN BUGS OF COQ V7.0
-
-- Realizer and Program/Program_all are not available
-
-- Local definitions in Record/Structure are not allowed
-
-- Alias of pattern with dependent types are not supported
-
-- Tokens with both symbols and letters are not supported
-
-- No consistency check is done when requiring a module (that is, a
-  module can be compiled with logical name Mycontrib.Arith.Plus but
-  required with name HisContrib.Zarith.Plus).
-
-- The syntax "Specialize num ident" is temporarily not accepted
-  outside "Tactic Definition". Syntax "Specialize ident" is OK.
-
-- New Induction fails for mutual inductive elimination
-
-- Elim fails with eliminators not imported
\ No newline at end of file
diff --git a/Makefile.build b/Makefile.build
index 0d0125ca..19f13f15 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -6,7 +6,7 @@
 #         #       GNU Lesser General Public License Version 2.1       #
 #######################################################################
 
-# $Id: Makefile.build 11858 2009-01-26 13:27:23Z notin $ 
+# $Id: Makefile.build 11935 2009-02-17 16:14:07Z notin $ 
 
 
 # Makefile for Coq
@@ -197,7 +197,7 @@ $(CHICKENOPT): checker/check.cmxa checker/main.ml
 
 $(CHICKENBYTE): checker/check.cma checker/main.ml
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) -o $@ str.cma unix.cma gramlib.cma $^
+	$(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ str.cma unix.cma gramlib.cma $^
 
 $(CHICKEN): $(ORDER_ONLY_SEP) $(BESTCHICKEN)
 	cd bin && ln -sf coqchk.$(BEST)$(EXE) coqchk$(EXE)
@@ -501,11 +501,13 @@ install-pcoq-manpages:
 # tests
 ###########################################################################
 
+VALIDOPTS=-silent -o -m
+
 validate:: $(BESTCHICKEN) $(ALLVO)
 	$(SHOW)'COQCHK <theories & contrib>'
-	$(HIDE)$(BESTCHICKEN) -boot -o -m $(ALLMODS)
+	$(HIDE)$(BESTCHICKEN) -boot $(VALIDOPTS) $(ALLMODS)
 
-check:: world
+check:: world validate
 	cd test-suite; \
 	env COQBIN=../bin COQLIB=.. ./check -$(BEST) | tee check.log
 	if grep -F 'Error!' test-suite/check.log ; then false; fi
@@ -590,29 +592,71 @@ printers: $(DEBUGPRINTERS)
 
 tools:: $(TOOLS) $(DEBUGPRINTERS)
 
+ifeq ($(BEST),opt)
+$(COQDEP): $(COQDEPCMX)
+	$(SHOW)'OCAMLOPT -o $@'
+	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ str.cmxa unix.cmxa gramlib.cmxa $^ $(OSDEPLIBS)
+	$(STRIP) $@
+else
 $(COQDEP): $(COQDEPCMO)
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma gramlib.cma $^ $(OSDEPLIBS)
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ str.cma unix.cma gramlib.cma $^ $(OSDEPLIBS)
+endif
 
+ifeq ($(BEST),opt)
+$(GALLINA): $(GALLINACMX)
+	$(SHOW)'OCAMLOPT -o $@'
+	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ $(GALLINACMX)
+	$(STRIP) $@
+else
 $(GALLINA): $(GALLINACMO)
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ $(GALLINACMO)
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ $(GALLINACMO)
+endif
 
+ifeq ($(BEST),opt)
+$(COQMAKEFILE): tools/coq_makefile.cmx config/coq_config.cmx
+	$(SHOW)'OCAMLOPT -o $@'
+	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ str.cmxa config/coq_config.cmx tools/coq_makefile.cmx
+	$(STRIP) $@
+else
 $(COQMAKEFILE): tools/coq_makefile.cmo config/coq_config.cmo
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma config/coq_config.cmo tools/coq_makefile.cmo
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ str.cma config/coq_config.cmo tools/coq_makefile.cmo
+endif
 
+ifeq ($(BEST),opt)
+$(COQTEX): tools/coq-tex.cmx
+	$(SHOW)'OCAMLOPT -o $@'
+	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ str.cmxa tools/coq-tex.cmx
+	$(STRIP) $@
+else
 $(COQTEX): tools/coq-tex.cmo
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma tools/coq-tex.cmo
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ str.cma tools/coq-tex.cmo
+endif
 
+ifeq ($(BEST),opt)
+$(COQWC): tools/coqwc.cmx
+	$(SHOW)'OCAMLOPT -o $@'
+	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ tools/coqwc.cmx
+	$(STRIP) $@
+else
 $(COQWC): tools/coqwc.cmo
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ tools/coqwc.cmo
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ tools/coqwc.cmo
+endif
 
+ifeq ($(BEST),opt)
+$(COQDOC): $(COQDOCCMX)
+	$(SHOW)'OCAMLOPT -o $@'
+	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ str.cmxa unix.cmxa $(COQDOCCMX)
+	$(STRIP) $@
+else
 $(COQDOC): $(COQDOCCMO)
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma $(COQDOCCMO)
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ str.cma unix.cma $(COQDOCCMO)
+endif
 
 ###########################################################################
 # Installation
@@ -639,13 +683,13 @@ install-binaries:: install-$(BEST) install-tools
 
 install-byte::
 	$(MKDIR) $(FULLBINDIR)
-	$(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(FULLBINDIR)
-	cd $(FULLBINDIR); ln -sf coqtop.byte$(EXE) coqtop$(EXE)
+	$(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(CHICKEN) $(FULLBINDIR)
+	cd $(FULLBINDIR); ln -sf coqtop.byte$(EXE) coqtop$(EXE); ln -sf coqchk.byte$(EXE) coqchk$(EXE)
 
 install-opt::
 	$(MKDIR) $(FULLBINDIR)
-	$(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(COQTOPOPT) $(FULLBINDIR)
-	cd $(FULLBINDIR); ln -sf coqtop.opt$(EXE) coqtop$(EXE)
+	$(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(COQTOPOPT) $(CHICKEN) $(CHICKENOPT) $(FULLBINDIR)
+	cd $(FULLBINDIR); ln -sf coqtop.opt$(EXE) coqtop$(EXE); ln -sf coqchk.opt$(EXE) coqchk$(EXE)
 
 install-tools::
 	$(MKDIR) $(FULLBINDIR)
diff --git a/Makefile.common b/Makefile.common
index 1889afc8..15faace0 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -66,8 +66,7 @@ COQTEX:=bin/coq-tex$(EXE)
 COQWC:=bin/coqwc$(EXE)
 COQDOC:=bin/coqdoc$(EXE)
 
-TOOLS:=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) \
-      $(COQWC) $(COQDOC)
+TOOLS:=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQWC) $(COQDOC)
 
 ###########################################################################
 # Documentation
@@ -404,11 +403,15 @@ CSDPCERTCMX:= $(CSDPCERTCMO:.cmo=.cmx)
 DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/printers.cma
 
 COQDEPCMO:=$(COQENVCMO) tools/coqdep_lexer.cmo tools/coqdep.cmo
+COQDEPCMX:=$(COQDEPCMO:.cmo=.cmx)
+
 GALLINACMO:=tools/gallina_lexer.cmo tools/gallina.cmo
+GALLINACMX:=$(GALLINACMO:.cmo=.cmx)
+
 COQDOCCMO:=$(CONFIG) tools/coqdoc/cdglobals.cmo tools/coqdoc/alpha.cmo \
 	tools/coqdoc/index.cmo tools/coqdoc/output.cmo \
 	tools/coqdoc/pretty.cmo tools/coqdoc/main.cmo
-
+COQDOCCMX:=$(COQDOCCMO:.cmo=.cmx)
 
 # checker
 
@@ -418,15 +421,15 @@ MCHECKER:=\
   lib/flags.cmo lib/util.cmo lib/option.cmo lib/hashcons.cmo \
   lib/system.cmo lib/envars.cmo \
   lib/predicate.cmo lib/rtree.cmo \
-  kernel/names.cmo kernel/univ.cmo \
-  kernel/esubst.cmo checker/term.cmo \
+  kernel/names.cmo kernel/univ.cmo kernel/esubst.cmo \
+  checker/validate.cmo \
+  checker/term.cmo \
   checker/declarations.cmo checker/environ.cmo \
   checker/closure.cmo checker/reduction.cmo \
   checker/type_errors.cmo \
   checker/modops.cmo \
   checker/inductive.cmo checker/typeops.cmo \
   checker/indtypes.cmo checker/subtyping.cmo checker/mod_checking.cmo \
-  checker/validate.cmo \
   checker/safe_typing.cmo checker/check.cmo \
   checker/check_stat.cmo checker/checker.cmo
 
diff --git a/README b/README
index 86783630..5cf88c1d 100644
--- a/README
+++ b/README
@@ -11,9 +11,8 @@ INSTALLATION.
 DOCUMENTATION.
 ==============
 
-   The documentation of Coq V8.2 is available by anonymous ftp (see below),
-   in a directory doc/. It is also available on Coq web site at
-   http://coq.inria.fr/doc-eng.html.
+   The documentation of Coq V8.2 is available online from the Coq web
+   site (see http://coq.inria.fr)
 
 
 CHANGES.
@@ -27,10 +26,10 @@ CHANGES.
 AVAILABILITY.
 =============
 
-   Coq is available by anonymous FTP on ftp.inria.fr:
+   Coq is available as a precompiled package from the major linux
+   distributions. It is also available for Windows and Mac OS systems
+   from the Coq web site (see http://coq.inria.fr).
 
-	host:	    ftp.inria.fr (192.93.2.54)
-	directory:  INRIA/LogiCal/coq/
 
 THE COQ CLUB.
 =============
@@ -68,11 +67,7 @@ BUGS REPORT.
 
    Send your bug reports by filling a form at
 
-        http://coq.inria.fr/bin/coq-bugs
-
-   or by E-mail to
-
-	coq-bugs@coq.inria.fr
+        http://logical.saclay.inria.fr/coq-bugs
 
    To be effective, bug reports should mention the Caml version used
    to compile and run Coq, the Coq version (coqtop -v), the configuration
diff --git a/README.win b/README.win
index af1df482..da1a456c 100644
--- a/README.win
+++ b/README.win
@@ -1,7 +1,7 @@
 THE COQ V8.2 SYSTEM
 ===================
 
-    This file contains remarks specific to the windows port of Coq.
+    This file contains remarks specific to the Windows port of Coq.
 
 INSTALLATION.
 =============
@@ -16,12 +16,19 @@ default).
 COMPILATION.
 ============
 
-    If you want to install coq, you had better transfer the precompiled
+    If you want to install Coq, you had better transfer the precompiled
     distribution. If you really need to recompile under Windows, here
     are some indications:
 
-    1- Install ocaml for Windows (MinGW port), preferably version 3.09.3.
+    1- Install OCaml for Windows (MinGW port), preferably version 3.11.0.
        See: http://caml.inria.fr
+     
+       If you choose OCaml 3.11.0, you also need to install FlexDLL.
+       See: http://alain.frisch.fr/flexdll.html    
+  
+       As shell script really dislikes space character within file
+       names, we strongly advise you to install OCaml to a path not
+       containing spaces, like 'C:\OCaml'
 
     2- Install a shell environment with at least:
          - a C compiler (gcc),
@@ -31,19 +38,22 @@ COMPILATION.
        (official packages are made using Cygwin) See:
        http://www.cygwin.com
 
-    3- In order to compile Coqide, you will need the LablGTK library
+    3- If using OCaml version >= 3.10.0, you have to install Camlp5.
+       See http://pauillac.inria.fr/~ddr/camlp5/
+
+    4- In order to compile Coqide, you will need the LablGTK library
        See: http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/lablgtk.html
 
        You also need to install the GTK libraries for Windows (see the
        installation instruction for LablGTK)
 
-    4- In a shell window, type successively
+    5- In a shell window, type successively
 
         ./configure
         make world
         make install
 
-    5- Though not nescessary, you can find useful:
+    6- Though not nescessary, you can find useful:
          - Windows version of (X)Emacs: it is a powerful environment for
            developpers with coloured syntax, modes for compilation and debug,
            and many more. It is free. See: http://www.gnu.org/software.
diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index 96366594..6ea153a3 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -55,7 +55,7 @@ let print_context env =
        env_stratification=
         {env_universes=univ; env_engagement=engt}} = env in
     msgnl(hov 0
-      (str"CONTEXT SUMMARY" ++ fnl() ++
+      (fnl() ++ str"CONTEXT SUMMARY" ++ fnl() ++
       str"===============" ++ fnl() ++ fnl() ++
       str "* " ++ hov 0 (pr_engt engt ++ fnl()) ++ fnl() ++
       str "* " ++ hov 0 (pr_ax csts) ++
@@ -65,5 +65,3 @@ let print_context env =
 let stats () =
   print_context (Safe_typing.get_env());
   print_memory_stat ()
-
-let _ = at_exit stats
diff --git a/checker/checker.ml b/checker/checker.ml
index 3d928933..70e2eb97 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -256,7 +256,7 @@ let rec explain_exn = function
   | Not_found -> 
       hov 0 (anomaly_string () ++ str "uncaught exception Not_found" ++ report ())
   | Failure s -> 
-      hov 0 (anomaly_string () ++ str "uncaught exception Failure " ++ str (guill s) ++ report ())
+      hov 0 (str "Failure: " ++ str s ++ report ())
   | Invalid_argument s -> 
       hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ str (guill s) ++ report ())
   | Sys.Break -> 
@@ -385,4 +385,4 @@ let run () =
     flush_all(); 
     exit 1)
 
-let start () = init(); run(); exit 0
+let start () = init(); run(); Check_stat.stats(); exit 0
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 2cf3854a..c6a7b4b4 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -1,6 +1,7 @@
 open Util
 open Names
 open Term
+open Validate
 
 (* Bytecode *)
 type values
@@ -11,17 +12,22 @@ type action
 type retroknowledge
 
 type engagement = ImpredicativeSet
+let val_eng = val_enum "eng" 1
 
 
 type polymorphic_arity = {
   poly_param_levels : Univ.universe option list;
   poly_level : Univ.universe;
 }
+let val_pol_arity =
+  val_tuple"polyorphic_arity"[|val_list(val_opt val_univ);val_univ|]
 
 type constant_type =
   | NonPolymorphicType of constr
   | PolymorphicArity of rel_context * polymorphic_arity
 
+let val_cst_type =
+  val_sum "constant_type" 0 [|[|val_constr|];[|val_rctxt;val_pol_arity|]|]
 
 
 type substitution_domain = 
@@ -29,6 +35,9 @@ type substitution_domain =
   | MBI of mod_bound_id
   | MPI of module_path
 
+let val_subst_dom =
+  val_sum "substitution_domain" 0 [|[|val_uid|];[|val_uid|];[|val_mp|]|]
+
 module Umap = Map.Make(struct 
 			 type t = substitution_domain
 			 let compare = Pervasives.compare
@@ -39,6 +48,13 @@ type resolver
 type substitution = (module_path * resolver option) Umap.t
 type 'a subst_fun = substitution -> 'a -> 'a
 
+let val_res = val_opt no_val
+
+let val_subst =
+  val_map ~name:"substitution"
+    val_subst_dom (val_tuple "substition range" [|val_mp;val_res|])
+
+
 let fold_subst fs fb fp =
   Umap.fold
     (fun k (mp,_) acc ->
@@ -360,6 +376,11 @@ let force_constr = force subst_mps
 
 type constr_substituted = constr substituted
 
+let val_cstr_subst =
+  val_ref
+    (val_sum "constr_substituted" 0
+      [|[|val_constr|];[|val_subst;val_constr|]|])
+
 let subst_constr_subst = subst_substituted
 
 type constant_body = {
@@ -372,6 +393,11 @@ type constant_body = {
     const_opaque : bool; 
     const_inline : bool}
 
+let val_cb = val_tuple "constant_body"
+  [|val_nctxt;val_opt val_cstr_subst; val_cst_type;no_val;val_cstrs;
+    val_bool; val_bool |]
+
+
 let subst_rel_declaration sub (id,copt,t as x) =
   let copt' = Option.smartmap (subst_mps sub) copt in
   let t' = subst_mps sub t in
@@ -383,6 +409,8 @@ type recarg =
   | Norec 
   | Mrec of int 
   | Imbr of inductive
+let val_recarg = val_sum "recarg" 1 (* Norec *)
+  [|[|val_int|] (* Mrec *);[|val_ind|] (* Imbr *)|]
 
 let subst_recarg sub r = match r with
   | Norec | Mrec _  -> r
@@ -390,6 +418,12 @@ let subst_recarg sub r = match r with
       if kn==kn' then r else Imbr (kn',i)
 
 type wf_paths = recarg Rtree.t
+let val_wfp = val_rec_sum "wf_paths" 0
+  (fun val_wfp -> 
+    [|[|val_int;val_int|]; (* Rtree.Param *)
+      [|val_recarg;val_array val_wfp|]; (* Rtree.Node *)
+      [|val_int;val_array val_wfp|] (* Rtree.Rec *)
+    |])
 
 let mk_norec = Rtree.mk_node Norec [||]
 
@@ -417,10 +451,14 @@ type monomorphic_inductive_arity = {
   mind_user_arity : constr;
   mind_sort : sorts;
 }
+let val_mono_ind_arity =
+  val_tuple"monomorphic_inductive_arity"[|val_constr;val_sort|]
 
 type inductive_arity = 
 | Monomorphic of monomorphic_inductive_arity
 | Polymorphic of polymorphic_arity
+let val_ind_arity = val_sum "inductive_arity" 0
+  [|[|val_mono_ind_arity|];[|val_pol_arity|]|]
 
 type one_inductive_body = {
 
@@ -471,6 +509,12 @@ type one_inductive_body = {
     mind_reloc_tbl :  reloc_table; 
   }
 
+let val_one_ind = val_tuple "one_inductive_body"
+  [|val_id;val_rctxt;val_ind_arity;val_array val_id;val_array val_constr;
+    val_int; val_list val_sortfam;val_array val_constr;val_array val_int;
+    val_wfp; val_int; val_int; no_val|]
+
+
 type mutual_inductive_body = {
 
   (* The component of the mutual inductive block *)
@@ -503,6 +547,10 @@ type mutual_inductive_body = {
   (* Source of the inductive block when aliased in a module *)
     mind_equiv : kernel_name option
   }
+let val_ind_pack = val_tuple "mutual_inductive_body"
+  [|val_array val_one_ind;val_bool;val_bool;val_int;val_nctxt;
+    val_int; val_int; val_rctxt;val_cstrs;val_opt val_kn|]
+
 
 let subst_arity sub = function
 | NonPolymorphicType s -> NonPolymorphicType (subst_mps sub s)
@@ -558,6 +606,8 @@ let subst_mind sub mib =
 
 (* Modules *)
 
+(* Whenever you change these types, please do update the validation
+   functions below *)
 type structure_field_body = 
   | SFBconst of constant_body
   | SFBmind of mutual_inductive_body
@@ -592,6 +642,30 @@ and module_type_body =
       typ_strength : module_path option;
       typ_alias : substitution}
 
+(* the validation functions: *)
+let rec val_sfb o = val_sum "struct_field_body" 0
+  [|[|val_cb|];       (* SFBconst *)
+    [|val_ind_pack|]; (* SFBmind *)
+    [|val_module|];   (* SFBmodule *)
+    [|val_mp;val_opt val_seb;val_opt val_cstrs|]; (* SFBalias *)
+    [|val_modtype|]   (* SFBmodtype *)
+  |] o
+and val_sb o = val_list (val_tuple"label*sfb"[|val_id;val_sfb|]) o
+and val_seb o = val_sum "struct_expr_body" 0
+  [|[|val_mp|];                      (* SEBident *)
+    [|val_uid;val_modtype;val_seb|]; (* SEBfunctor *)
+    [|val_uid;val_sb|];              (* SEBstruct *)
+    [|val_seb;val_seb;val_cstrs|];   (* SEBapply *)
+    [|val_seb;val_with|]             (* SEBwith *)
+  |] o
+and val_with o = val_sum "with_declaration_body" 0
+  [|[|val_list val_id;val_mp;val_cstrs|];
+    [|val_list val_id;val_cb|]|] o
+and val_module o = val_tuple "module_body"
+  [|val_opt val_seb;val_opt val_seb;val_cstrs;val_subst;no_val|] o
+and val_modtype o = val_tuple "module_type_body"
+  [|val_seb;val_opt val_mp;val_subst|] o
+
 	
 let rec subst_with_body sub = function
   | With_module_body(id,mp,typ_opt,cst) ->
diff --git a/checker/declarations.mli b/checker/declarations.mli
index 78bf2053..d71e625f 100644
--- a/checker/declarations.mli
+++ b/checker/declarations.mli
@@ -212,3 +212,8 @@ val join_alias : substitution -> substitution -> substitution
 val update_subst_alias : substitution -> substitution -> substitution
 val update_subst : substitution -> substitution -> substitution
 val subst_key : substitution -> substitution -> substitution
+
+(* Validation *)
+val val_eng : Obj.t -> unit
+val val_module : Obj.t -> unit
+val val_modtype : Obj.t -> unit
diff --git a/checker/environ.ml b/checker/environ.ml
index 58f08bdd..4bdbeee6 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -201,6 +201,3 @@ let lookup_module mp env =
 
 let lookup_modtype ln env = 
   MPmap.find ln env.env_globals.env_modtypes
-
-let lookup_alias mp env =
-  MPmap.find mp env.env_globals.env_alias
diff --git a/checker/environ.mli b/checker/environ.mli
index a3f531dd..1541bf0d 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -1,6 +1,8 @@
 open Names
 open Term
 
+(* Environments *)
+
 type globals = {
   env_constants : Declarations.constant_body Cmap.t;
   env_inductives : Declarations.mutual_inductive_body KNmap.t;
@@ -20,26 +22,33 @@ type env = {
   env_imports : Digest.t MPmap.t;
 }
 val empty_env : env
+
+(* Engagement *)
 val engagement : env -> Declarations.engagement option
-val universes : env -> Univ.universes
-val named_context : env -> named_context
-val rel_context : env -> rel_context
 val set_engagement : Declarations.engagement -> env -> env
 
+(* Digests *)
 val add_digest : env -> dir_path -> Digest.t -> env
 val lookup_digest : env -> dir_path -> Digest.t
 
+(* de Bruijn variables *)
+val rel_context : env -> rel_context
 val lookup_rel : int -> env -> rel_declaration
 val push_rel : rel_declaration -> env -> env
 val push_rel_context : rel_context -> env -> env
 val push_rec_types : name array * constr array * 'a -> env -> env
 
+(* Named variables *)
+val named_context : env -> named_context
 val push_named : named_declaration -> env -> env
 val lookup_named : identifier -> env -> named_declaration
 val named_type : identifier -> env -> constr
 
+(* Universes *)
+val universes : env -> Univ.universes
 val add_constraints : Univ.constraints -> env -> env
 
+(* Constants *)
 val lookup_constant : constant -> env -> Declarations.constant_body
 val add_constant : constant -> Declarations.constant_body -> env -> env
 val constant_type : env -> constant -> Declarations.constant_type
@@ -49,6 +58,7 @@ val constant_value : env -> constant -> constr
 val constant_opt_value : env -> constant -> constr option
 val evaluable_constant : constant -> env -> bool
 
+(* Inductives *)
 val lookup_mind :
   mutual_inductive -> env -> Declarations.mutual_inductive_body
 val scrape_mind : env -> mutual_inductive -> mutual_inductive
@@ -56,6 +66,7 @@ val add_mind :
   mutual_inductive -> Declarations.mutual_inductive_body -> env -> env
 val mind_equiv : env -> inductive -> inductive -> bool
 
+(* Modules *)
 val add_modtype :
   module_path -> Declarations.module_type_body -> env -> env
 val shallow_add_module :
@@ -64,4 +75,3 @@ val register_alias : module_path -> module_path -> env -> env
 val scrape_alias : module_path -> env -> module_path
 val lookup_module : module_path -> env -> Declarations.module_body
 val lookup_modtype : module_path -> env -> Declarations.module_type_body
-val lookup_alias : module_path -> env -> module_path
diff --git a/checker/include b/checker/include
new file mode 100644
index 00000000..331eb45c
--- /dev/null
+++ b/checker/include
@@ -0,0 +1,176 @@
+(* -*-tuareg-*- *)
+
+(* Caml script to include for debugging the checker.
+   Usage: from the checker/ directory launch ocaml toplevel and then
+   type #use"include";;
+   This command loads the relevent modules, defines some pretty
+   printers, and provides functions to interactively check modules
+   (mainly run_l and norec).
+ *)
+
+#cd ".."
+#directory "lib";;
+#directory "kernel";;
+#directory "checker";;
+
+#load "unix.cma";;
+#load "str.cma";;
+#load "gramlib.cma";;
+#load "check.cma";;
+
+open Typeops;;
+open Check;;
+
+
+open Pp;;
+open Util;;
+open Names;;
+open Term;;
+open Environ;;
+open Declarations;;
+open Mod_checking;;
+
+let pr_id id = str(string_of_id id)
+let pr_na = function Name id -> pr_id id | _ -> str"_";;
+let prdp dp = pp(str(string_of_dirpath dp));;
+(*
+let prc c = pp(Himsg.pr_lconstr_env (Check.get_env()) c);;
+let prcs cs = prc (Declarations.force cs);;
+let pru u = pp(str(Univ.string_of_universe u));;*)
+let pru u = pp(Univ.pr_uni u);;
+let prlab l = pp(str(string_of_label l));;
+let prid id = pp(pr_id id);;
+let prcon c = pp(Indtypes.prcon c);;
+let prkn kn = pp(Indtypes.prkn kn);;
+
+
+let prus g = pp(Univ.pr_universes g);;
+
+let prcstrs c =
+  let g = Univ.merge_constraints c Univ.initial_universes in
+  pp(Univ.pr_universes g);;
+(*let prcstrs c = pp(Univ.pr_constraints c);; *)
+(*
+let prenvu e =
+  let u = universes e in
+  let pu =
+  str "UNIVERSES:"++fnl()++str"  "++hov 0 (Univ.pr_universes u) ++fnl() in
+  pp pu;;
+
+let prenv e =
+  let ctx1 = named_context e in
+  let ctx2 = rel_context e in
+  let pe =
+    hov 1 (str"[" ++
+           prlist_with_sep spc (fun (na,_,_) -> pr_id na) (List.rev ctx1)++
+           str"]") ++ spc() ++
+    hov 1 (str"[" ++
+           prlist_with_sep spc (fun (na,_,_) -> pr_na na) (List.rev ctx2)++
+           str"]") in
+  pp pe;;
+*)
+
+let prsub s =
+  let string_of_mp mp =
+    let s = string_of_mp mp in
+    (match mp with MPself _ -> "#self."|MPbound _ -> "#bound."|_->"")^s in 
+  pp (hv 0 
+  (fold_subst
+    (fun msid mp strm ->
+      str "S " ++ str (debug_string_of_msid msid) ++ str " |-> " ++
+      str (string_of_mp mp) ++ fnl() ++ strm)
+    (fun mbid mp strm ->
+      str"B " ++ str (debug_string_of_mbid mbid) ++ str " |-> " ++
+      str (string_of_mp mp) ++ fnl() ++ strm)
+    (fun mp1 mp strm ->
+      str"P " ++ str (string_of_mp mp1) ++ str " |-> " ++
+      str (string_of_mp mp) ++ fnl() ++ strm) s (mt())))
+;;
+
+#install_printer prid;;
+#install_printer prcon;;
+#install_printer prlab;;
+#install_printer prdp;;
+#install_printer prkn;;
+#install_printer pru;;
+(*
+#install_printer prc;;
+#install_printer prcs;;
+*)
+#install_printer prcstrs;;
+(*#install_printer prus;;*)
+(*#install_printer prenv;;*)
+(*#install_printer prenvu;;*)
+#install_printer prsub;;
+
+Checker.init();;
+Flags.make_silent false;;
+Flags.debug := true;;
+Sys.catch_break true;;
+
+let module_of_file f =
+  let (_,mb,_,_) = Obj.magic ((intern_from_file f).library_compiled) in
+  (mb:module_body)
+;;
+let mod_access m fld =
+  match m.mod_expr with
+      Some(SEBstruct(msid,l)) -> List.assoc fld l
+    | _ -> failwith "bad structure type"
+;;
+
+let parse_dp s =
+  make_dirpath(List.map id_of_string (List.rev (Str.split(Str.regexp"\\.") s)))
+;;
+let parse_sp s =
+  let l = List.rev (Str.split(Str.regexp"\\.") s) in
+  {dirpath=List.tl l; basename=List.hd l};;
+let parse_kn s =
+   let l = List.rev (Str.split(Str.regexp"\\.") s) in
+   let dp = make_dirpath(List.map id_of_string(List.tl l)) in
+   make_kn(MPfile dp) empty_dirpath (label_of_id (id_of_string (List.hd l)))
+;;
+let parse_con s =
+   let l = List.rev (Str.split(Str.regexp"\\.") s) in
+   let dp = make_dirpath(List.map id_of_string(List.tl l)) in
+   make_con(MPfile dp) empty_dirpath (label_of_id (id_of_string (List.hd l)))
+;;
+let get_mod dp = 
+  lookup_module dp (Safe_typing.get_env())
+;;
+let get_mod_type dp = 
+  lookup_modtype dp (Safe_typing.get_env())
+;;
+let get_cst kn = 
+  lookup_constant kn (Safe_typing.get_env())
+;;
+
+let read_mod s f = 
+  let lib = intern_from_file (parse_dp s,f) in
+  ((Obj.magic lib.library_compiled):
+    dir_path *
+    module_body *
+    (dir_path * Digest.t) list *
+    engagement option);;
+
+let deref_mod md s =
+  let (Some (SEBstruct(msid,l))) = md.mod_expr in
+  List.assoc (label_of_id(id_of_string s)) l
+;;
+
+let expln f x =
+  try f x
+  with UserError(_,strm) as e ->
+    msgnl strm; raise e
+
+let admit_l l =
+  let l = List.map parse_sp l in
+  Check.recheck_library ~admit:l ~check:l;;
+let run_l l =
+  Check.recheck_library ~admit:[] ~check:(List.map parse_sp l);;
+let norec q =
+  Check.recheck_library ~norec:[parse_sp q] ~admit:[] ~check:[];;
+
+(*
+admit_l["Bool";"OrderedType";"DecidableType"];;
+run_l["FSetInterface"];;
+*)
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index af5e4f46..9e7a2336 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -130,6 +130,12 @@ let check_definition_sub env cb1 cb2 =
 	Reduction.conv env c1 c2
     | _ -> ())
 
+let lookup_modtype mp env =
+  try Environ.lookup_modtype mp env
+  with Not_found ->
+    failwith ("Unknown module type: "^string_of_mp mp)
+
+
 let rec check_with env mtb with_decl = 
   match with_decl with
     | With_definition_body _ -> 
@@ -308,7 +314,8 @@ and check_structure_field (s,env) mp lab = function
 
 and check_modexpr env mse = match mse with
   | SEBident mp ->
-      let mtb = lookup_modtype mp env in 
+      let mp = scrape_alias mp env in
+      let mtb = lookup_modtype mp env in
       mtb.typ_alias
   | SEBfunctor (arg_id, mtb, body) ->
       check_module_type env mtb;
diff --git a/checker/modops.ml b/checker/modops.ml
index 27ea4d55..498bd775 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -125,6 +125,7 @@ let strengthen_mind env mp l mib = match mib.mind_equiv with
 let rec eval_struct env = function 
   | SEBident mp -> 
       begin
+        let mp = scrape_alias mp env in
 	let mtb =lookup_modtype mp env in
 	match mtb.typ_expr,mtb.typ_strength with
 	    mtb,None -> eval_struct env mtb
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index d5779923..9e886837 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -106,6 +106,10 @@ type compiled_library =
     (dir_path * Digest.t) list *
     engagement option
  
+open Validate
+let val_deps = val_list (val_tuple"dep"[|val_dp;no_val|])
+let val_vo = val_tuple "vo" [|val_dp;val_module;val_deps;val_eng|]
+
 (* This function should append a certificate to the .vo file.
    The digest must be part of the certicate to rule out attackers
    that could change the .vo file between the time it was read and
@@ -116,7 +120,7 @@ let stamp_library file digest = ()
 (* When the module is checked, digests do not need to match, but a
    warning is issued in case of mismatch *)
 let import file (dp,mb,depends,engmt as vo) digest = 
-  Validate.val_vo (Obj.repr vo);
+  Validate.apply !Flags.debug val_vo vo;
   Flags.if_verbose msgnl (str "*** vo structure validated ***");
   let env = !genv in
   check_imports msg_warning dp env depends;
diff --git a/checker/term.ml b/checker/term.ml
index 45568a59..f245d155 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -15,6 +15,7 @@ open Pp
 open Names
 open Univ
 open Esubst
+open Validate
 
 (* Coq abstract syntax with deBruijn variables; 'a is the type of sorts *)
 
@@ -35,6 +36,10 @@ type case_info =
     ci_cstr_nargs : int array; (* number of real args of each constructor *)
     ci_pp_info    : case_printing (* not interpreted by the kernel *)
   }
+let val_ci =
+  let val_cstyle = val_enum "case_style" 5 in
+  let val_cprint = val_tuple "case_printing" [|val_int;val_cstyle|] in
+  val_tuple "case_info" [|val_ind;val_int;val_array val_int;val_cprint|]
 
 (* Sorts. *)
 
@@ -51,6 +56,9 @@ let family_of_sort = function
   | Prop Pos -> InSet
   | Type _ -> InType
 
+let val_sort = val_sum "sort" 0 [|[|val_enum "cnt" 2|];[|val_univ|]|]
+let val_sortfam = val_enum "sorts_family" 3
+
 (********************************************************************)
 (*       Constructions as implemented                               *)
 (********************************************************************)
@@ -65,7 +73,16 @@ type 'constr pfixpoint =
 type 'constr pcofixpoint =
     int * 'constr prec_declaration
 
+let val_evar f = val_tuple "pexistential" [|val_int;val_array f|]
+let val_prec f =
+  val_tuple "prec_declaration"[|val_array val_name; val_array f; val_array f|]
+let val_fix f =
+  val_tuple"pfixpoint"
+    [|val_tuple"fix2"[|val_array val_int;val_int|];val_prec f|]
+let val_cofix f = val_tuple"pcofixpoint"[|val_int;val_prec f|]
+
 type cast_kind = VMcast | DEFAULTcast 
+let val_cast = val_enum "cast_kind" 2
 
 (*s*******************************************************************)
 (* The type of constructions *)
@@ -88,11 +105,31 @@ type constr =
   | Fix       of constr pfixpoint
   | CoFix     of constr pcofixpoint
 
+let val_constr = val_rec_sum "constr" 0 (fun val_constr -> [|
+  [|val_int|]; (* Rel *)
+  [|val_id|]; (* Var *)
+  [|val_int|]; (* Meta *)
+  [|val_evar val_constr|]; (* Evar *)
+  [|val_sort|]; (* Sort *)
+  [|val_constr;val_cast;val_constr|]; (* Cast *)
+  [|val_name;val_constr;val_constr|]; (* Prod *)
+  [|val_name;val_constr;val_constr|]; (* Lambda *)
+  [|val_name;val_constr;val_constr;val_constr|]; (* LetIn *)
+  [|val_constr;val_array val_constr|]; (* App *)
+  [|val_kn|]; (* Const *)
+  [|val_ind|]; (* Ind *)
+  [|val_cstr|]; (* Construct *)
+  [|val_ci;val_constr;val_constr;val_array val_constr|]; (* Case *)
+  [|val_fix val_constr|]; (* Fix *)
+  [|val_cofix val_constr|] (* CoFix *)
+|])
+
 type existential = constr pexistential
 type rec_declaration = constr prec_declaration
 type fixpoint = constr pfixpoint
 type cofixpoint = constr pcofixpoint
 
+
 let rec strip_outer_cast c = match c with
   | Cast (c,_,_) -> strip_outer_cast c
   | _ -> c
@@ -275,6 +312,13 @@ let subst1 lam = substl [lam]
 (*     Type of assumptions and contexts                                    *)
 (***************************************************************************)
 
+let val_ndecl =
+  val_tuple"named_declaration"[|val_id;val_opt val_constr;val_constr|]
+let val_rdecl =
+  val_tuple"rel_declaration"[|val_name;val_opt val_constr;val_constr|]
+let val_nctxt = val_list val_ndecl
+let val_rctxt = val_list val_rdecl
+
 type named_declaration = identifier * constr option * constr
 type rel_declaration = name * constr option * constr
 
@@ -395,6 +439,7 @@ let decompose_prod_n_assum n =
 (***************************)
 
 type arity = rel_context * sorts
+let val_arity = val_tuple"arity"[|val_rctxt;val_constr|]
 
 let mkArity (sign,s) = it_mkProd_or_LetIn (Sort s) sign
 
diff --git a/checker/term.mli b/checker/term.mli
index 30a2c03a..1367e581 100644
--- a/checker/term.mli
+++ b/checker/term.mli
@@ -109,3 +109,10 @@ val destArity : constr -> arity
 val isArity : constr -> bool
 val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool
 val eq_constr : constr -> constr -> bool
+
+(* Validation *)
+val val_sortfam : Obj.t -> unit
+val val_sort : Obj.t -> unit
+val val_constr : Obj.t -> unit
+val val_rctxt : Obj.t -> unit
+val val_nctxt : Obj.t -> unit
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 1af8b2ce..1832ebec 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -140,7 +140,10 @@ let type_of_constant env cst =
 
 let judge_of_constant_knowing_parameters env cst paramstyp =
   let c = Const cst in
-  let cb = lookup_constant cst env in
+  let cb =
+    try lookup_constant cst env 
+    with Not_found ->
+      failwith ("Cannot find constant: "^string_of_con cst) in
   let _ = check_args env c cb.const_hyps in 
   type_of_constant_knowing_parameters env cb.const_type paramstyp
 
@@ -222,7 +225,10 @@ let judge_of_cast env (c,cj) k tj =
 
 let judge_of_inductive_knowing_parameters env ind (paramstyp:constr array) =
   let c = Ind ind in
-  let (mib,mip) = lookup_mind_specif env ind in
+  let (mib,mip) =
+    try lookup_mind_specif env ind
+    with Not_found ->
+      failwith ("Cannot find inductive: "^string_of_kn (fst ind)) in
   check_args env c mib.mind_hyps;
   type_of_inductive_knowing_parameters env mip paramstyp
 
@@ -235,7 +241,10 @@ let judge_of_constructor env c =
   let constr = Construct c in
   let _ =
     let ((kn,_),_) = c in
-    let mib = lookup_mind kn env in
+    let mib = 
+      try lookup_mind kn env
+      with Not_found ->
+        failwith ("Cannot find inductive: "^string_of_kn (fst (fst c))) in
     check_args env constr mib.mind_hyps in 
   let specif = lookup_mind_specif env (inductive_of_constructor c) in
   type_of_constructor c specif
diff --git a/checker/validate.ml b/checker/validate.ml
index 86e51b7b..804bf7df 100644
--- a/checker/validate.ml
+++ b/checker/validate.ml
@@ -6,19 +6,19 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: term.ml 10098 2007-08-27 11:41:08Z herbelin $ *)
+(* $Id$ *)
 
 (* This module defines validation functions to ensure an imported
    value (using input_value) has the correct structure. *)
 
 let rec pr_obj_rec o =
   if Obj.is_int o then
-    Format.print_string ("INT:"^string_of_int(Obj.magic o))
+    Format.print_int(Obj.magic o)
   else if Obj.is_block o then
     let t = Obj.tag o in
     if t > Obj.no_scan_tag then
       if t = Obj.string_tag then
-        Format.print_string ("STR:"^Obj.magic o)
+        Format.print_string ("\""^String.escaped(Obj.magic o)^"\"")
       else
         Format.print_string "?"
     else
@@ -36,7 +36,20 @@ let rec pr_obj_rec o =
 let pr_obj o = pr_obj_rec o; Format.print_newline()
 
 (**************************************************************************)
-(* Low-level validators *)
+(* Obj low-level validators *)
+
+exception ValidObjError of string * Obj.t
+let fail o s = raise (ValidObjError(s,o))
+
+let apply debug f x =
+  let o = Obj.repr x in
+  try f o
+  with ValidObjError(msg,obj) ->
+    if debug then begin
+      print_endline ("Validation failed: "^msg);
+      pr_obj obj
+    end;
+    failwith "validation failed"
 
 (* data not validated *)
 let no_val (o:Obj.t) = ()
@@ -44,26 +57,24 @@ let no_val (o:Obj.t) = ()
 (* Check that object o is a block with tag t *)
 let val_tag t o =
   if Obj.is_block o && Obj.tag o = t then ()
-  else failwith ("tag "^string_of_int t)
+  else fail o ("expected tag "^string_of_int t)
 
-let val_obj s o =
+let val_block s o =
   if Obj.is_block o then
     (if Obj.tag o > Obj.no_scan_tag then
-      failwith (s^". Not a normal tag"))
-  else failwith (s^". Not a block")
+      fail o (s^": found no scan tag"))
+  else fail o (s^": expected block obj")
 
 (* Check that an object is a tuple (or a record). v is an array of
    validation functions for each field. Its size corresponds to the
    expected size of the object. *)
 let val_tuple s v o =
   let n = Array.length v in
-  val_obj ("tuple: "^s) o;
+  val_block ("tuple: "^s) o;
   if Obj.size o = n then
     Array.iteri (fun i f -> f (Obj.field o i)) v
   else
-    (pr_obj o;
-     failwith
-       ("tuple:" ^s^" size found:"^string_of_int (Obj.size o)))
+    fail o ("tuple:" ^s^" size found:"^string_of_int (Obj.size o))
 
 (* Check that the object is either a constant constructor of tag < cc,
    or a constructed variant. each element of vv is an array of
@@ -73,15 +84,16 @@ let val_tuple s v o =
    i-th non-constant constructor. *)
 let val_sum s cc vv o =
   if Obj.is_block o then
-    (val_obj ("sum: "^s) o;
+    (val_block s o;
     let n = Array.length vv in
     let i = Obj.tag o in
-    if i < n then val_tuple (s^"("^string_of_int i^")") vv.(i) o
-    else failwith ("bad tag in sum ("^s^"): "^string_of_int i))
+    if i < n then val_tuple (s^"(tag "^string_of_int i^")") vv.(i) o
+    else fail o ("bad tag in (sum type) "^s^": max is "^string_of_int i))
   else if Obj.is_int o then
     let (n:int) = Obj.magic o in
-    (if n<0 || n>=cc then failwith ("bad constant constructor ("^s^")"))
-  else failwith ("not a sum ("^s^")")
+    (if n<0 || n>=cc then
+      fail o (s^": bad constant constructor "^string_of_int n))
+  else fail o ("not a sum ("^s^")")
 
 let val_enum s n = val_sum s n [||]
 
@@ -89,177 +101,79 @@ let val_enum s n = val_sum s n [||]
 let rec val_rec_sum s cc f o =
   val_sum s cc (f (val_rec_sum s cc f)) o
 
+let rec val_rectype f o =
+  f (val_rectype f) o
+
 (**************************************************************************)
 (* Builtin types *)
 
 (* Check the o is an array of values satisfying f. *)
-let val_array f o =
-  val_obj "array" o;
+let val_array ?(name="array") f o =
+  val_block name o;
   for i = 0 to Obj.size o - 1 do
     (f (Obj.field o i):unit)
   done
 
 (* Integer validator *)
 let val_int o =
-  if not (Obj.is_int o) then failwith "expected an int"
+  if not (Obj.is_int o) then fail o "expected an int"
 
 (* String validator *)
-let val_str s = val_tag Obj.string_tag s
+let val_str o =
+  try val_tag Obj.string_tag o
+  with Failure _ -> fail o "expected a string"
 
 (* Booleans *)
 let val_bool = val_enum "bool" 2
 
 (* Option type *)
-let val_opt f = val_sum "option" 1 [|[|f|]|]
+let val_opt ?(name="option") f = val_sum name 1 [|[|f|]|]
 
 (* Lists *)
-let val_list f =
-  val_rec_sum "list" 1 (fun vlist -> [|[|f;vlist|]|])
+let val_list ?(name="list") f =
+  val_rec_sum name 1 (fun vlist -> [|[|f;vlist|]|])
 
 (* Reference *)
-let val_ref f = val_tuple "ref" [|f|]
+let val_ref ?(name="ref") f = val_tuple name [|f|]
 
 (**************************************************************************)
 (* Standard library types *)
 
 (* Sets *)
-let val_set f =
-  val_rec_sum "set" 1 (fun vset -> [|[|vset;f;vset;val_int|]|])
+let val_set ?(name="Set.t") f =
+  val_rec_sum name 1 (fun vset -> [|[|vset;f;vset;val_int|]|])
 
 (* Maps *)
-let rec val_map fk fv =
-  val_rec_sum "map" 1 (fun vmap -> [|[|vmap;fk;fv;vmap;val_int|]|])
+let rec val_map ?(name="Map.t") fk fv =
+  val_rec_sum name 1 (fun vmap -> [|[|vmap;fk;fv;vmap;val_int|]|])
 
 (**************************************************************************)
 (* Coq types *)
 
+(* names *)
 let val_id = val_str
 
-let val_dp = val_list val_id
+let val_dp = val_list ~name:"dirpath" val_id
 
 let val_name = val_sum "name" 1 [|[|val_id|]|]
 
-let val_uid = val_tuple "uid" [|val_int;val_str;val_dp|]
+let val_uid = val_tuple "uniq_ident" [|val_int;val_str;val_dp|]
 
 let val_mp =
-  val_rec_sum "mp" 0
+  val_rec_sum "module_path" 0
     (fun vmp -> [|[|val_dp|];[|val_uid|];[|val_uid|];[|vmp;val_id|]|])
 
-let val_kn = val_tuple "kn" [|val_mp;val_dp;val_id|]
-
-let val_ind = val_tuple "ind"[|val_kn;val_int|]
-let val_cstr = val_tuple "cstr"[|val_ind;val_int|]
-
-let val_ci =
-  let val_cstyle = val_enum "case_style" 5 in
-  let val_cprint = val_tuple "case_printing" [|val_int;val_cstyle|] in
-  val_tuple "case_info" [|val_ind;val_int;val_array val_int;val_cprint|]
+let val_kn = val_tuple "kernel_name" [|val_mp;val_dp;val_id|]
 
+let val_ind = val_tuple "inductive"[|val_kn;val_int|]
+let val_cstr = val_tuple "constructor"[|val_ind;val_int|]
 
+(* univ *)
 let val_level = val_sum "level" 1 [|[|val_dp;val_int|]|]
 let val_univ = val_sum "univ" 0
   [|[|val_level|];[|val_list val_level;val_list val_level|]|]
 
 let val_cstrs =
-  val_set (val_tuple"univ_cstr"[|val_level;val_enum "order" 3;val_level|])
-
-let val_cast = val_enum "cast_kind" 2
-let val_sort = val_sum "sort" 0 [|[|val_enum "cnt" 2|];[|val_univ|]|]
-let val_sortfam = val_enum "sort_family" 3
-
-let val_evar f = val_tuple "evar" [|val_int;val_array f|]
-
-let val_prec f =
-  val_tuple "prec"[|val_array val_name; val_array f; val_array f|]
-let val_fix f =
-  val_tuple"fix1"[|val_tuple"fix2"[|val_array val_int;val_int|];val_prec f|]
-let val_cofix f = val_tuple"cofix"[|val_int;val_prec f|]
-
-
-let val_constr = val_rec_sum "constr" 0 (fun val_constr -> [|
-  [|val_int|]; (* Rel *)
-  [|val_id|]; (* Var *)
-  [|val_int|]; (* Meta *)
-  [|val_evar val_constr|]; (* Evar *)
-  [|val_sort|]; (* Sort *)
-  [|val_constr;val_cast;val_constr|]; (* Cast *)
-  [|val_name;val_constr;val_constr|]; (* Prod *)
-  [|val_name;val_constr;val_constr|]; (* Lambda *)
-  [|val_name;val_constr;val_constr;val_constr|]; (* LetIn *)
-  [|val_constr;val_array val_constr|]; (* App *)
-  [|val_kn|]; (* Const *)
-  [|val_ind|]; (* Ind *)
-  [|val_cstr|]; (* Construct *)
-  [|val_ci;val_constr;val_constr;val_array val_constr|]; (* Case *)
-  [|val_fix val_constr|]; (* Fix *)
-  [|val_cofix val_constr|] (* CoFix *)
-|])
-
-
-let val_ndecl = val_tuple"ndecl"[|val_id;val_opt val_constr;val_constr|]
-let val_rdecl = val_tuple"rdecl"[|val_name;val_opt val_constr;val_constr|]
-let val_nctxt = val_list val_ndecl
-let val_rctxt = val_list val_rdecl
-
-let val_arity = val_tuple"arity"[|val_rctxt;val_constr|]
-
-let val_eng = val_enum "eng" 1
-
-let val_pol_arity = val_tuple"pol_arity"[|val_list(val_opt val_univ);val_univ|]
-let val_cst_type =
-  val_sum "cst_type" 0 [|[|val_constr|];[|val_rctxt;val_pol_arity|]|]
-
-let val_subst_dom =
-  val_sum "subst_dom" 0 [|[|val_uid|];[|val_uid|];[|val_mp|]|]
-
-
-let val_res = val_opt no_val
-
-let val_subst =
-  val_map val_subst_dom (val_tuple "subst range" [|val_mp;val_res|])
-
-let val_cstr_subst =
-  val_ref (val_sum "cstr_subst" 0 [|[|val_constr|];[|val_subst;val_constr|]|])
-
-let val_cb = val_tuple "cb"
-  [|val_nctxt;val_opt val_cstr_subst; val_cst_type;no_val;val_cstrs;
-    val_bool; val_bool |]
-
-let val_recarg = val_sum "recarg" 1 [|[|val_int|];[|val_ind|]|]
-
-let val_wfp = val_rec_sum "wf_paths" 0
-  (fun val_wfp -> 
-    [|[|val_int;val_int|];[|val_recarg;val_array val_wfp|];
-      [|val_int;val_array val_wfp|]|])
-
-let val_mono_ind_arity = val_tuple"mono_ind_arity"[|val_constr;val_sort|]
-let val_ind_arity = val_sum "ind_arity" 0
-  [|[|val_mono_ind_arity|];[|val_pol_arity|]|]
-
-let val_one_ind = val_tuple "one_ind"
-  [|val_id;val_rctxt;val_ind_arity;val_array val_id;val_array val_constr;
-    val_int; val_list val_sortfam;val_array val_constr;val_array val_int;
-    val_wfp; val_int; val_int; no_val|]
-
-let val_ind_pack = val_tuple "ind_pack"
-  [|val_array val_one_ind;val_bool;val_bool;val_int;val_nctxt;
-    val_int; val_int; val_rctxt;val_cstrs;val_opt val_kn|]
-
-let rec val_sfb o = val_sum "sfb" 0
-  [|[|val_cb|];[|val_ind_pack|];[|val_mod|];
-    [|val_mp;val_opt val_cstrs|];[|val_modty|]|] o
-and val_sb o = val_list (val_tuple"sb"[|val_id;val_sfb|]) o
-and val_seb o = val_sum "seb" 0
-  [|[|val_mp|];[|val_uid;val_modty;val_seb|];[|val_uid;val_sb|];
-    [|val_seb;val_seb;val_cstrs|];[|val_seb;val_with|]|] o
-and val_with o = val_sum "with" 0
-  [|[|val_list val_id;val_mp;val_cstrs|];
-    [|val_list val_id;val_cb|]|] o
-and val_mod o = val_tuple "module_body"
-  [|val_opt val_seb;val_opt val_seb;val_cstrs;val_subst;no_val|] o
-and val_modty o = val_tuple "module_type_body"
-  [|val_seb;val_opt val_mp;val_subst|] o
-
-let val_deps = val_list (val_tuple"dep"[|val_dp;no_val|])
-
-let val_vo = val_tuple "vo" [|val_dp;val_mod;val_deps;val_eng|]
+  val_set ~name:"Univ.constraints"
+   (val_tuple "univ_constraint"
+     [|val_level;val_enum "order_request" 3;val_level|])
diff --git a/config/Makefile.template b/config/Makefile.template
index 35e2a2d7..6f9fac3c 100644
--- a/config/Makefile.template
+++ b/config/Makefile.template
@@ -23,6 +23,7 @@ LOCAL=LOCALINSTALLATION
 
 # Bytecode link flags for VM ("-custom" or "-dllib -lcoqrun")
 COQRUNBYTEFLAGS=XCOQRUNBYTEFLAGS
+COQTOOLSBYTEFLAGS=XCOQTOOLSBYTEFLAGS
 BUILDLDPATH=
 
 # Paths for true installation
diff --git a/configure b/configure
index 14ff9950..c8508f52 100755
--- a/configure
+++ b/configure
@@ -6,9 +6,9 @@
 # 
 ##################################
 
-VERSION=8.2rc2
-VOMAGIC=08193 
-STATEMAGIC=19764
+VERSION=8.2
+VOMAGIC=08200 
+STATEMAGIC=58200
 DATE=`LANG=C date +"%B %Y"`
 
 # Create the bin/ directory if non-existent
@@ -36,7 +36,11 @@ usage () {
     echo "-local"
     printf "\tSet installation directory to the current source tree\n"
     echo "-coqrunbyteflags"
-    printf "\tSet link flags for VM-dependent bytecode\n"
+    printf "\tSet link flags for VM-dependent bytecode (coqtop)\n"
+    echo "-coqtoolsbyteflags"
+    printf "\tSet link flags for VM-independant bytecode (coqdep, coqdoc, ...)\n"
+    echo "-custom"
+    printf "\tGenerate all bytecode executables with -custom (not recommended)\n"
     echo "-src"
     printf "\tSpecifies the source directory\n"
     echo "-bindir"
@@ -111,6 +115,8 @@ ranlib_exec=ranlib
 
 local=false
 coqrunbyteflags_spec=no
+coqtoolsbyteflags_spec=no
+custom_spec=no
 src_spec=no
 prefix_spec=no
 bindir_spec=no
@@ -147,6 +153,11 @@ while : ; do
     -coqrunbyteflags|--coqrunbyteflags) coqrunbyteflags_spec=yes
                                         coqrunbyteflags="$2"
                                         shift;;
+    -coqtoolsbyteflags|--coqtoolsbyteflags) coqtoolsbyteflags_spec=yes
+                                            coqtoolsbyteflags="$2"
+                                            shift;;
+    -custom|--custom) custom_spec=yes
+                      shift;;
     -src|--src) src_spec=yes
                 COQSRC="$2"
 	        shift;;
@@ -388,7 +399,7 @@ fi
 
 # Under Windows, OCaml only understands Windows filenames (C:\...)
 case $ARCH in
-    win32) CAMLBIN=`cygpath -w ${CAMLBIN}`;;
+    win32) CAMLBIN=`cygpath -m ${CAMLBIN}`;;
 esac
 
 # this fixes a camlp4 bug under FreeBSD
@@ -668,7 +679,7 @@ esac
 
 # OCaml only understand Windows filenames (C:\...)
 case $ARCH in
-    win32) COQTOP=`cygpath -w ${COQTOP}`
+    win32) COQTOP=`cygpath -m ${COQTOP}`
 esac
 
 case $ARCH in
@@ -774,12 +785,25 @@ case $coqdocdir_spec/$prefix_spec/$local in
 	esac;;
 esac
 
+# Determine if we enable -custom by default (Windows and MacOS)
+CUSTOM_OS=no
+if [ "$ARCH" = "win32" ] || [ "`uname -s`" = "Darwin" ]; then
+    CUSTOM_OS=yes
+fi
+
 BUILDLDPATH="# you might want to set CAML_LD_LIBRARY_PATH by hand!"
-case $coqrunbyteflags_spec/$local 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";;
+case $coqrunbyteflags_spec/$local/$custom_spec/$CUSTOM_OS in
+    yes/*/*/*) COQRUNBYTEFLAGS="$coqrunbyteflags";;
+    */*/yes/*|*/*/*/yes) COQRUNBYTEFLAGS="-custom";;
+    */true/*/*) COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath '$COQTOP'/kernel/byterun";;
+    *)
+        COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath '$LIBDIR'"
+        BUILDLDPATH="export CAML_LD_LIBRARY_PATH='$COQTOP'/kernel/byterun";;
+esac
+case $coqtoolsbyteflags_spec/$custom_spec/$CUSTOM_OS in
+    yes/*/*) COQTOOLSBYTEFLAGS="$coqtoolsbyteflags";;
+    */yes/*|*/*/yes) COQTOOLSBYTEFLAGS="-custom";;
+    *) COQTOOLSBYTEFLAGS="";;
 esac
 
 # case $emacs_spec in
@@ -803,6 +827,7 @@ if test ! -z "$OS" ; then
   echo "  Operating system                  : $OS"
 fi
 echo "  Coq VM bytecode link flags        : $COQRUNBYTEFLAGS"
+echo "  Coq tools bytecode link flags     : $COQTOOLSBYTEFLAGS"
 echo "  OS dependent libraries            : $OSDEPLIBS"
 echo "  Objective-Caml/Camlp4 version     : $CAMLVERSION"
 echo "  Objective-Caml/Camlp4 binaries in : $CAMLBIN"
@@ -858,7 +883,7 @@ case $ARCH in
     win32)
 	ESCCOQTOP=`echo $COQTOP |sed -e 's|\\\|\\\\\\\|g'`
 	ESCBINDIR=`echo $BINDIR |sed -e 's|\\\|\\\\\\\|g'`
-	ESCSRCDIR=`cygpath -d $COQSRC |sed -e 's|\\\|\\\\\\\|g'`
+	ESCSRCDIR=`cygpath -m $COQSRC |sed -e 's|\\\|\\\\\\\|g'`
 	ESCLIBDIR=`echo $LIBDIR |sed -e 's|\\\|\\\\\\\|g'`
 	ESCCAMLDIR=`echo $CAMLBIN |sed -e 's|\\\|\\\\\\\|g'`
 	ESCCAMLLIB=`echo $CAMLLIB |sed -e 's|\\\|\\\\\\\|g'`
@@ -870,6 +895,7 @@ case $ARCH in
 	ESCCAMLP4LIB=`echo $CAMLP4LIB |sed -e 's|\\\|\\\\\\\|g'`
 	ESCLABLGTKINCLUDES=`echo $LABLGTKINCLUDES |sed -e 's|\\\|\\\\\\\|g'`
 	ESCCOQRUNBYTEFLAGS=`echo $COQRUNBYTEFLAGS |sed -e 's|\\\|\\\\\\\|g'`
+	ESCCOQTOOLSBYTEFLAGS=`echo $COQTOOLSBYTEFLAGS |sed -e 's|\\\|\\\\\\\|g'`
 	ESCBUILDLDPATH=`echo $BUILDLDPATH |sed -e 's|\\\|\\\\\\\|g'`
 ;;
     *)
@@ -887,6 +913,7 @@ case $ARCH in
    	ESCCAMLP4LIB="$CAMLP4LIB"
 	ESCLABLGTKINCLUDES="$LABLGTKINCLUDES"
 	ESCCOQRUNBYTEFLAGS="$COQRUNBYTEFLAGS"
+	ESCCOQTOOLSBYTEFLAGS="$COQTOOLSBYTEFLAGS"
 	;;
 esac
 
@@ -947,6 +974,7 @@ rm -f "$COQSRC/config/Makefile"
 
 sed -e "s|LOCALINSTALLATION|$local|" \
     -e "s|XCOQRUNBYTEFLAGS|$ESCCOQRUNBYTEFLAGS|" \
+    -e "s|XCOQTOOLSBYTEFLAGS|$ESCCOQTOOLSBYTEFLAGS|" \
     -e "s|COQSRCDIRECTORY|$COQSRC|" \
     -e "s|COQVERSION|$VERSION|" \
     -e "s|BINDIRDIRECTORY|$ESCBINDIR|" \
@@ -1040,4 +1068,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 11858 2009-01-26 13:27:23Z notin $
+# $Id: configure 11934 2009-02-17 15:58:54Z notin $
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index fa006c1c..2cf457c6 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: extraction.ml 11459 2008-10-16 16:29:07Z letouzey $ i*)
+(*i $Id: extraction.ml 11897 2009-02-09 19:28:02Z barras $ i*)
 
 (*i*)
 open Util
@@ -177,7 +177,7 @@ let parse_ind_args si args relmax =
 
 
 let rec extract_type env db j c args = 
-  match kind_of_term (whd_betaiotazeta c) with
+  match kind_of_term (whd_betaiotazeta Evd.empty c) with
     | App (d, args') ->
 	(* We just accumulate the arguments. *)
 	extract_type env db j d (Array.to_list args' @ args)
@@ -285,7 +285,7 @@ and extract_type_app env db (r,s) args =
 and extract_type_scheme env db c p = 
   if p=0 then extract_type env db 0 c [] 
   else 
-    let c = whd_betaiotazeta c in 
+    let c = whd_betaiotazeta Evd.empty c in 
     match kind_of_term c with 
       | Lambda (n,t,d) -> 
           extract_type_scheme (push_rel_assum (n,t) env) db d (p-1)
diff --git a/contrib/firstorder/unify.ml b/contrib/firstorder/unify.ml
index 1dd13cbe..27c06f54 100644
--- a/contrib/firstorder/unify.ml
+++ b/contrib/firstorder/unify.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: unify.ml 7639 2005-12-02 10:01:15Z gregoire $ i*)
+(*i $Id: unify.ml 11897 2009-02-09 19:28:02Z barras $ i*)
 
 open Util
 open Formula 
@@ -42,8 +42,8 @@ let unif t1 t2=
     Queue.add (t1,t2) bige;
     try while true do
       let t1,t2=Queue.take bige in
-      let nt1=head_reduce (whd_betaiotazeta t1) 
-      and nt2=head_reduce (whd_betaiotazeta t2) in
+      let nt1=head_reduce (whd_betaiotazeta Evd.empty t1) 
+      and nt2=head_reduce (whd_betaiotazeta Evd.empty t2) in
 	match (kind_of_term nt1),(kind_of_term nt2) with
 	    Meta i,Meta j-> 
 	      if i<>j then 
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index 9f3e412a..b13bea9d 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -252,7 +252,8 @@ let change_eq env sigma hyp_id (context:Sign.rel_context) x t end_of_type  =
 	(new_end_of_type,0,witness_fun)
 	context
     in
-    let new_type_of_hyp = Reductionops.nf_betaiota  new_type_of_hyp in 
+    let new_type_of_hyp =
+      Reductionops.nf_betaiota Evd.empty new_type_of_hyp in 
     let new_ctxt,new_end_of_type = 
       Sign.decompose_prod_n_assum ctxt_size new_type_of_hyp 
     in 
@@ -708,7 +709,8 @@ let build_proof
 		  | Const _ ->
 		      do_finalize dyn_infos  g
 		  | Lambda _ -> 
-		      let new_term = Reductionops.nf_beta dyn_infos.info in 
+		      let new_term =
+                        Reductionops.nf_beta Evd.empty dyn_infos.info in 
 		      build_proof do_finalize {dyn_infos with info = new_term} 
 			g
 		  | LetIn _ -> 
@@ -1056,7 +1058,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 	    let bodies_with_all_params = 
 	      Array.map 
 		(fun body -> 
-		   Reductionops.nf_betaiota 
+		   Reductionops.nf_betaiota Evd.empty
 		     (applist(substl (List.rev (Array.to_list all_funs_with_full_params)) body,
 			      List.rev_map var_of_decl princ_params))
 		)
@@ -1093,12 +1095,12 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 		   let body_with_param,num = 
 		     let body = get_body fnames.(i) in 
 		     let body_with_full_params = 
-		       Reductionops.nf_betaiota (
+		       Reductionops.nf_betaiota Evd.empty (
 			 applist(body,List.rev_map var_of_decl full_params))
 		     in
 		     match kind_of_term body_with_full_params with 
 		       | Fix((_,num),(_,_,bs)) -> 
-			       Reductionops.nf_betaiota
+			       Reductionops.nf_betaiota Evd.empty
 				 (
 				   (applist
 				      (substl 
@@ -1174,7 +1176,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 		     nb_rec_hyps = -100;
 		     rec_hyps = [];
 		     info = 
-		       Reductionops.nf_betaiota 
+		       Reductionops.nf_betaiota Evd.empty
 			 (applist(fix_body,List.rev_map mkVar args_id));
 		     eq_hyps = []
 		   }
@@ -1236,7 +1238,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 		     nb_rec_hyps = -100;
 		     rec_hyps = [];
 		     info = 
-		       Reductionops.nf_betaiota 
+		       Reductionops.nf_betaiota Evd.empty 
 			 (applist(fbody_with_full_params,
 				  (List.rev_map var_of_decl princ_params)@
 				    (List.rev_map mkVar args_id)
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index cf861642..2ab62763 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -1361,7 +1361,7 @@ and natural_cutintro ig lh g gs arg ltree =
                        {ihsg=No_subgoals_hyp;isgintro=""}
                        (List.nth ltree 0))]
         ]
-and whd_betadeltaiota x = whd_betaiotaevar (Global.env()) Evd.empty x
+and whd_betadeltaiota x = whd_betaiota Evd.empty x
 and type_of_ast s c = type_of (Global.env()) Evd.empty (constr_of_ast c)
 and prod_head t =
   match (kind_of_term (strip_outer_cast t)) with 
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index 094226ff..1d213db9 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: subtac_cases.ml 11576 2008-11-10 19:13:15Z msozeau $ *)
+(* $Id: subtac_cases.ml 11897 2009-02-09 19:28:02Z barras $ *)
 
 open Cases
 open Util
@@ -822,7 +822,7 @@ let infer_predicate loc env isevars typs cstrs indf =
     (* Empiric normalization: p may depend in a irrelevant way on args of the*)
     (* cstr as in [c:{_:Alpha & Beta}] match c with (existS a b)=>(a,b) end *)
     let typs =
-      Array.map (local_strong (whd_betaevar empty_env (Evd.evars_of !isevars))) typs
+      Array.map (local_strong whd_beta (Evd.evars_of !isevars)) typs
     in
     let eqns = array_map2 prepare_unif_pb typs cstrs in
     (* First strategy: no dependencies at all *)
@@ -1042,9 +1042,10 @@ let find_predicate loc env isevars p typs cstrs current
     match p with
       | Some p -> abstract_predicate env (Evd.evars_of !isevars) indf current tms p
       | None -> infer_predicate loc env isevars typs cstrs indf in
-  let typ = whd_beta (applist (pred, realargs)) in
+  let typ = whd_beta (Evd.evars_of !isevars) (applist (pred, realargs)) in
   if dep then
-    (pred, whd_beta (applist (typ, [current])), new_Type ())
+    (pred, whd_beta (Evd.evars_of !isevars) (applist (typ, [current])),
+     new_Type ())
   else
     (pred, typ, new_Type ())
 
@@ -1246,7 +1247,7 @@ and match_current pb tomatch =
 	    find_predicate pb.caseloc pb.env pb.isevars 
 	      pb.pred brtyps cstrs current indt pb.tomatch in
 	  let ci = make_case_info pb.env mind pb.casestyle in
-	  let case = mkCase (ci,nf_betaiota pred,current,brvals) in
+	  let case = mkCase (ci,nf_betaiota Evd.empty pred,current,brvals) in
 	  let inst = List.map mkRel deps in
 	  { uj_val = applist (case, inst);
 	    uj_type = substl inst typ }
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index cc1e2dde..d2e831ef 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -282,7 +282,7 @@ let declare_obligation obl body =
 	print_message (Subtac_utils.definition_message obl.obl_name);
 	{ obl with obl_body = Some (mkConst constant) }
 	  
-let red = Reductionops.nf_betaiota
+let red = Reductionops.nf_betaiota Evd.empty
 
 let init_prog_info n b t deps fixkind notations obls impls kind hook =
   let obls' = 
diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml
index c62db00b..13e5e6d5 100644
--- a/contrib/xml/cic2acic.ml
+++ b/contrib/xml/cic2acic.ml
@@ -245,9 +245,9 @@ let typeur sigma metamap =
         let Inductiveops.IndType(_,realargs) =
           try Inductiveops.find_rectype env sigma (type_of env c)
           with Not_found -> Util.anomaly "type_of: Bad recursive type" in
-        let t = Reductionops.whd_beta (T.applist (p, realargs)) in
+        let t = Reductionops.whd_beta sigma (T.applist (p, realargs)) in
         (match Term.kind_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma (type_of env t)) with
-          | T.Prod _ -> Reductionops.whd_beta (T.applist (t, [c]))
+          | T.Prod _ -> Reductionops.whd_beta sigma (T.applist (t, [c]))
           | _ -> t)
     | T.Lambda (name,c1,c2) ->
           T.mkProd (name, c1, type_of (Environ.push_rel (name,None,c1) env) c2)
@@ -390,7 +390,7 @@ Pp.ppnl (Pp.(++) (Pp.str "BUG: this subterm was not visited during the double-ty
           (* We need to refresh the universes because we are doing *)
           (* type inference on an already inferred type.           *)
           {D.synthesized =
-            Reductionops.nf_beta
+            Reductionops.nf_beta evar_map
              (CPropRetyping.get_type_of env evar_map
               (Termops.refresh_universes tt)) ;
            D.expected = None}
diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml
index de8c540c..17d1d5da 100644
--- a/contrib/xml/doubleTypeInference.ml
+++ b/contrib/xml/doubleTypeInference.ml
@@ -163,7 +163,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
            | hj::restjl ->
               match T.kind_of_term (Reduction.whd_betadeltaiota env typ) with
                  T.Prod (_,c1,c2) ->
-                  (Some (Reductionops.nf_beta c1)) ::
+                  (Some (Reductionops.nf_beta sigma c1)) ::
                    (aux (T.subst1 hj c2) restjl)
                | _ -> assert false
          in
@@ -183,7 +183,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
           | Some ety ->
               match T.kind_of_term (Reduction.whd_betadeltaiota env ety) with
                  T.Prod (_,_,expected_target_type) ->
-                  Some (Reductionops.nf_beta expected_target_type)
+                  Some (Reductionops.nf_beta sigma expected_target_type)
                | _ -> assert false
         in
         let j' = execute env1 sigma c2 expectedc2type in 
@@ -214,14 +214,14 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
           Typeops.judge_of_letin env name j1 j2 j3
   
      | T.Cast (c,k,t) ->
-        let cj = execute env sigma c (Some (Reductionops.nf_beta t)) in
+        let cj = execute env sigma c (Some (Reductionops.nf_beta sigma t)) in
         let tj = execute env sigma t None in
 	let tj = type_judgment env sigma tj in
         let j, _ = Typeops.judge_of_cast env cj k tj in
 	 j
     in
      let synthesized = E.j_type judgement in
-     let synthesized' = Reductionops.nf_beta synthesized in
+     let synthesized' = Reductionops.nf_beta sigma synthesized in
       let types,res =
        match expectedty with
           None ->
diff --git a/dev/base_include b/dev/base_include
index 0b7a0b67..d4366843 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -128,7 +128,6 @@ open Hipattern
 open Inv
 open Leminv
 open Refine
-open Setoid_replace
 open Tacinterp
 open Tacticals
 open Tactics
diff --git a/ide/coq.ico b/ide/coq.ico
new file mode 100644
index 00000000..94ce897d
--- /dev/null
+++ b/ide/coq.ico
diff --git a/install.sh b/install.sh
index 0719ca77..277222f5 100755
--- a/install.sh
+++ b/install.sh
@@ -1,13 +1,13 @@
 #! /bin/sh
 
-dest=$1
+dest="$1"
 shift
 
 for f; do
   bn=`basename $f`
   dn=`dirname $f`
-  install -d $dest/$dn
-  install -m 644 $f $dest/$dn/$bn
+  install -d "$dest/$dn"
+  install -m 644 $f "$dest/$dn/$bn"
 done
 
 
diff --git a/interp/notation.ml b/interp/notation.ml
index fcb2b6f5..776fff79 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: notation.ml 11512 2008-10-27 12:28:36Z herbelin $ *)
+(* $Id: notation.ml 11897 2009-02-09 19:28:02Z barras $ *)
 
 (*i*)
 open Util
@@ -422,7 +422,7 @@ let find_class_scope cl =
   Gmap.find cl !class_scope_map
 
 let find_class t =
-  let t, _ = decompose_app (Reductionops.whd_betaiotazeta t) in
+  let t, _ = decompose_app (Reductionops.whd_betaiotazeta Evd.empty t) in
   match kind_of_term t with
     | Var id -> CL_SECVAR id
     | Const sp -> CL_CONST sp
@@ -435,7 +435,7 @@ let find_class t =
 (* Special scopes associated to arguments of a global reference *)
 
 let rec compute_arguments_scope t =
-  match kind_of_term (Reductionops.whd_betaiotazeta t) with
+  match kind_of_term (Reductionops.whd_betaiotazeta Evd.empty t) with
     | Prod (_,t,u) ->
 	let sc =
 	  try Some (find_class_scope (find_class t)) with Not_found -> None in
diff --git a/kernel/closure.ml b/kernel/closure.ml
index b85be204..a184c128 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: closure.ml 10819 2008-04-20 18:14:44Z msozeau $ *)
+(* $Id: closure.ml 11897 2009-02-09 19:28:02Z barras $ *)
 
 open Util
 open Pp
@@ -28,7 +28,8 @@ let iota = ref 0
 let prune = ref 0
 
 let reset () =
-  beta := 0; delta := 0; zeta := 0; evar := 0; iota := 0; prune := 0
+  beta := 0; delta := 0; zeta := 0; evar := 0; iota := 0; evar := 0;
+  prune := 0
 
 let stop() =
   msgnl (str "[Reds: beta=" ++ int !beta ++ str" delta=" ++ int !delta ++
@@ -83,7 +84,6 @@ module RedFlags = (struct
     r_delta : bool;
     r_const : transparent_state;
     r_zeta : bool;
-    r_evar : bool;
     r_iota : bool }
 
   type red_kind = BETA | DELTA | IOTA | ZETA
@@ -99,7 +99,6 @@ module RedFlags = (struct
     r_delta = false;
     r_const = all_opaque;
     r_zeta = false;
-    r_evar = false;
     r_iota = false }
 
   let red_add red = function
@@ -201,6 +200,7 @@ type 'a infos = {
   i_flags : reds;
   i_repr : 'a infos -> constr -> 'a;
   i_env : env;
+  i_sigma : existential -> constr option;
   i_rels : int * (int * constr) list;
   i_vars : (identifier * constr) list;
   i_tab : (table_key, 'a) Hashtbl.t }
@@ -227,6 +227,9 @@ let ref_value_cache info ref =
     | NotEvaluableConst _ (* Const *)
       -> None
 
+let evar_value info ev =
+  info.i_sigma ev
+
 let defined_vars flags env =
 (*  if red_local_const (snd flags) then*)
     Sign.fold_named_context 
@@ -259,10 +262,11 @@ let rec mind_equiv env (kn1,i1) (kn2,i2) =
 
 let mind_equiv_infos info = mind_equiv info.i_env
 
-let create mk_cl flgs env =
+let create mk_cl flgs env evars =
   { i_flags = flgs;
     i_repr = mk_cl;
     i_env = env;
+    i_sigma = evars;
     i_rels = defined_rels flgs env;
     i_vars = defined_vars flgs env;
     i_tab = Hashtbl.create 17 }
@@ -314,7 +318,7 @@ and fterm =
   | FLambda of int * (name * constr) list * constr * fconstr subs
   | FProd of name * fconstr * fconstr
   | FLetIn of name * fconstr * fconstr * constr * fconstr subs
-  | FEvar of existential_key * fconstr array
+  | FEvar of existential * fconstr subs
   | FLIFT of int * fconstr
   | FCLOS of constr * fconstr subs
   | FLOCKED
@@ -581,8 +585,8 @@ let mk_clos_deep clos_fun env t =
     | LetIn (n,b,t,c) ->
         { norm = Red;
 	  term = FLetIn (n, clos_fun env b, clos_fun env t, c, env) }
-    | Evar(ev,args) ->
-	{ norm = Whnf; term = FEvar(ev,Array.map (clos_fun env) args) }
+    | Evar ev ->
+	{ norm = Red; term = FEvar(ev,env) }
 
 (* A better mk_clos? *)
 let mk_clos2 = mk_clos_deep mk_clos
@@ -632,7 +636,8 @@ let rec to_constr constr_fun lfts v =
 	mkLetIn (n, constr_fun lfts b,
 	            constr_fun lfts t,
 	            constr_fun (el_lift lfts) fc)
-    | FEvar (ev,args) -> mkEvar(ev,Array.map (constr_fun lfts) args)
+    | FEvar ((ev,args),env) ->
+        mkEvar(ev,Array.map (fun a -> constr_fun lfts (mk_clos2 env a)) args)
     | FLIFT (k,a) -> to_constr constr_fun (el_shft k lfts) a
     | FCLOS (t,env) ->
         let fr = mk_clos2 env t in
@@ -891,6 +896,10 @@ let rec knr info m stk =
         | (_,args,s) -> (m,args@s))
   | FLetIn (_,v,_,bd,e) when red_set info.i_flags fZETA ->
       knit info (subs_cons([|v|],e)) bd stk
+  | FEvar(ev,env) ->
+      (match evar_value info ev with
+          Some c -> knit info env c stk
+        | None -> (m,stk))
   | _ -> (m,stk)
 
 (* Computes the weak head normal form of a term *)
@@ -959,7 +968,8 @@ and norm_head info m =
           let fbds =
             Array.map (mk_clos (subs_liftn (Array.length na) e)) bds in
           mkFix(n,(na, Array.map (kl info) ftys, Array.map (kl info) fbds))
-      | FEvar(i,args) -> mkEvar(i, Array.map (kl info) args)
+      | FEvar((i,args),env) ->
+          mkEvar(i, Array.map (fun a -> kl info (mk_clos env a)) args)
       | t -> term_of_fconstr m
 
 (* Initialization and then normalization *)
@@ -982,7 +992,7 @@ let whd_stack infos m stk =
 (* cache of constants: the body is computed only when needed. *)
 type clos_infos = fconstr infos
 
-let create_clos_infos flgs env =
-  create (fun _ -> inject) flgs env
+let create_clos_infos ?(evars=fun _ -> None) flgs env =
+  create (fun _ -> inject) flgs env evars
 
 let unfold_reference = ref_value_cache
diff --git a/kernel/closure.mli b/kernel/closure.mli
index c814baad..a80f7a62 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: closure.mli 10652 2008-03-10 21:52:06Z herbelin $ i*)
+(*i $Id: closure.mli 11897 2009-02-09 19:28:02Z barras $ i*)
 
 (*i*)
 open Pp
@@ -85,7 +85,9 @@ type table_key = id_key
 type 'a infos
 val ref_value_cache: 'a infos -> table_key -> 'a option
 val info_flags: 'a infos -> reds
-val create: ('a infos -> constr -> 'a) -> reds -> env -> 'a infos
+val create: ('a infos -> constr -> 'a) -> reds -> env ->
+  (existential -> constr option) -> 'a infos
+val evar_value : 'a infos -> existential -> constr option
 
 (************************************************************************)
 (*s Lazy reduction. *)
@@ -111,7 +113,7 @@ type fterm =
   | FLambda of int * (name * constr) list * constr * fconstr subs
   | FProd of name * fconstr * fconstr
   | FLetIn of name * fconstr * fconstr * constr * fconstr subs
-  | FEvar of existential_key * fconstr array
+  | FEvar of existential * fconstr subs
   | FLIFT of int * fconstr
   | FCLOS of constr * fconstr subs
   | FLOCKED
@@ -156,7 +158,8 @@ val destFLambda :
 
 (* Global and local constant cache *)
 type clos_infos
-val create_clos_infos : reds -> env -> clos_infos
+val create_clos_infos :
+  ?evars:(existential->constr option) -> reds -> env -> clos_infos
 
 (* Reduction function *)
 
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 43ef3a98..76b32463 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: reduction.ml 10930 2008-05-15 10:50:32Z barras $ *)
+(* $Id: reduction.ml 11897 2009-02-09 19:28:02Z barras $ *)
 
 open Util
 open Names
@@ -248,10 +248,12 @@ and eqappr cv_pb infos (lft1,st1) (lft2,st2) cuniv =
 	       then convert_stacks infos lft1 lft2 v1 v2 cuniv
                else raise NotConvertible
 	   | _ -> raise NotConvertible)
-    | (FEvar (ev1,args1), FEvar (ev2,args2)) ->
+    | (FEvar ((ev1,args1),env1), FEvar ((ev2,args2),env2)) ->
         if ev1=ev2 then
           let u1 = convert_stacks infos lft1 lft2 v1 v2 cuniv in
-          convert_vect infos el1 el2 args1 args2 u1
+          convert_vect infos el1 el2
+            (Array.map (mk_clos env1) args1)
+            (Array.map (mk_clos env2) args2) u1
         else raise NotConvertible
 
     (* 2 index known to be bound to no constant *)
@@ -382,29 +384,29 @@ and convert_vect infos lft1 lft2 v1 v2 cuniv =
     fold 0 cuniv
   else raise NotConvertible
 
-let clos_fconv trans cv_pb env t1 t2 =
-  let infos = trans, create_clos_infos betaiotazeta env in
+let clos_fconv trans cv_pb evars env t1 t2 =
+  let infos = trans, create_clos_infos ~evars betaiotazeta env in
   ccnv cv_pb infos ELID ELID (inject t1) (inject t2) Constraint.empty
 
-let trans_fconv reds cv_pb env t1 t2 =
+let trans_fconv reds cv_pb evars env t1 t2 =
   if eq_constr t1 t2 then Constraint.empty
-  else clos_fconv reds cv_pb env t1 t2
+  else clos_fconv reds cv_pb evars env t1 t2
 
-let trans_conv_cmp conv reds = trans_fconv reds conv
-let trans_conv reds = trans_fconv reds CONV
-let trans_conv_leq reds = trans_fconv reds CUMUL
+let trans_conv_cmp conv reds = trans_fconv reds conv (fun _->None)
+let trans_conv ?(evars=fun _->None) reds = trans_fconv reds CONV evars
+let trans_conv_leq ?(evars=fun _->None) reds = trans_fconv reds CUMUL evars
 
 let fconv = trans_fconv (Idpred.full, Cpred.full)
 
-let conv_cmp = fconv
-let conv = fconv CONV
-let conv_leq = fconv CUMUL
+let conv_cmp cv_pb = fconv cv_pb (fun _->None)
+let conv ?(evars=fun _->None) = fconv CONV evars
+let conv_leq ?(evars=fun _->None) = fconv CUMUL evars
 
-let conv_leq_vecti env v1 v2 =
+let conv_leq_vecti ?(evars=fun _->None) env v1 v2 =
   array_fold_left2_i 
     (fun i c t1 t2 ->
       let c' =
-        try conv_leq env t1 t2 
+        try conv_leq ~evars env t1 t2 
         with NotConvertible -> raise (NotConvertibleVect i) in
       Constraint.union c c')
     Constraint.empty
@@ -413,17 +415,17 @@ let conv_leq_vecti env v1 v2 =
 
 (* option for conversion *)
 
-let vm_conv = ref fconv
+let vm_conv = ref (fun cv_pb -> fconv cv_pb (fun _->None))
 let set_vm_conv f = vm_conv := f
 let vm_conv cv_pb env t1 t2 = 
   try 
     !vm_conv cv_pb env t1 t2
   with Not_found | Invalid_argument _ ->
       (* If compilation fails, fall-back to closure conversion *)
-      fconv cv_pb env t1 t2
+      fconv cv_pb (fun _->None) env t1 t2
   
 
-let default_conv = ref fconv 
+let default_conv = ref (fun cv_pb -> fconv cv_pb (fun _->None))
 
 let set_default_conv f = default_conv := f
 
@@ -432,7 +434,7 @@ let default_conv cv_pb env t1 t2 =
     !default_conv cv_pb env t1 t2
   with Not_found | Invalid_argument _ ->
       (* If compilation fails, fall-back to closure conversion *)
-      fconv cv_pb env t1 t2
+      fconv cv_pb (fun _->None) env t1 t2
   
 let default_conv_leq = default_conv CUMUL
 (*
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 3b9eb315..d8658d43 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: reduction.mli 10840 2008-04-23 21:29:34Z herbelin $ i*)
+(*i $Id: reduction.mli 11897 2009-02-09 19:28:02Z barras $ i*)
 
 (*i*)
 open Term
@@ -40,15 +40,18 @@ val conv_sort      : sorts conversion_function
 val conv_sort_leq  : sorts conversion_function
 
 val trans_conv_cmp       : conv_pb -> constr trans_conversion_function
-
-val trans_conv           : constr trans_conversion_function
-val trans_conv_leq       : types trans_conversion_function
+val trans_conv           :
+  ?evars:(existential->constr option) -> constr trans_conversion_function
+val trans_conv_leq       :
+  ?evars:(existential->constr option) -> types trans_conversion_function
 
 val conv_cmp       : conv_pb -> constr conversion_function
-
-val conv           : constr conversion_function
-val conv_leq       : types conversion_function
-val conv_leq_vecti : types array conversion_function
+val conv           :
+  ?evars:(existential->constr option) -> constr conversion_function
+val conv_leq       :
+  ?evars:(existential->constr option) -> types conversion_function
+val conv_leq_vecti :
+  ?evars:(existential->constr option) -> types array conversion_function
 
 (* option for conversion *)
 val set_vm_conv : (conv_pb -> types conversion_function) -> unit
diff --git a/lib/envars.ml b/lib/envars.ml
index 5887adcd..d700ffe1 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -21,8 +21,9 @@ let guess_coqlib () =
     else 
       let coqbin = System.canonical_path_name (Filename.dirname Sys.executable_name) in
       let prefix = Filename.dirname coqbin in
-      let coqlib = if Coq_config.local then prefix else 
-	List.fold_left Filename.concat prefix ["lib";"coq"] in
+      let rpath = if Coq_config.local then [] else 
+	  (if Coq_config.arch = "win32" then ["lib"] else ["lib";"coq"]) in
+      let coqlib = List.fold_left Filename.concat prefix rpath in
 	if Sys.file_exists (Filename.concat coqlib file) then coqlib else
 	  Util.error "cannot guess a path for Coq libraries; please use -coqlib option"
 	  
diff --git a/lib/util.ml b/lib/util.ml
index a73a5558..a8a99c0b 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id: util.ml 11845 2009-01-22 18:55:08Z letouzey $ *)
+(* $Id: util.ml 11897 2009-02-09 19:28:02Z barras $ *)
 
 open Pp
 
@@ -1354,6 +1354,39 @@ let pr_located pr (loc,x) =
 
 let surround p = hov 1 (str"(" ++ p ++ str")")
 
+(*s Memoization *)
+
+let memo1_eq eq f =
+  let m = ref None in
+  fun x ->
+    match !m with
+        Some(x',y') when eq x x' -> y'
+      | _ -> let y = f x in m := Some(x,y); y
+
+let memo1_1 f = memo1_eq (==) f
+let memo1_2 f =
+  let f' =
+    memo1_eq (fun (x,y) (x',y') -> x==x' && y==y') (fun (x,y) -> f x y) in
+  (fun x y -> f'(x,y))
+
+(* Memorizes the last n distinct calls to f. Since there is no hash,
+   Efficient only for small n. *)
+let memon_eq eq n f =
+  let cache = ref [] in (* the cache: a stack *)
+  let m = ref 0 in      (* usage of the cache *)
+  let rec find x = function
+    | (x',y')::l when eq x x' -> y', l (* cell is moved to the top *)
+    | [] -> (* we assume n>0, so creating one memo cell is OK *)
+        incr m; (f x, [])
+    | [_] when !m>=n -> f x,[] (* cache is full: dispose of last cell *)
+    | p::l (* not(eq x (fst p)) *) -> let (y,l') = find x l in (y, p::l')
+  in
+  (fun x ->
+    let (y,l) = find x !cache in
+    cache := (x,y)::l;
+    y)
+
+
 (*s Size of ocaml values. *)
 
 module Size = struct
diff --git a/lib/util.mli b/lib/util.mli
index 3cd934e7..5432eb98 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(*i $Id: util.mli 11769 2009-01-08 17:59:22Z glondu $ i*)
+(*i $Id: util.mli 11897 2009-02-09 19:28:02Z barras $ i*)
 
 (*i*)
 open Pp
@@ -298,6 +298,21 @@ val pr_located : ('a -> std_ppcmds) -> 'a located -> std_ppcmds
 val pr_sequence : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
 val surround : std_ppcmds -> std_ppcmds
 
+(*s Memoization. *)
+
+(* General comments on memoization:
+   - cache is created whenever the function is supplied (because of
+      ML's polymorphic value restriction).
+   - cache is never flushed (unless the memoized fun is GC'd)
+ *)
+(* One cell memory: memorizes only the last call *)
+val memo1_1 : ('a -> 'b) -> ('a -> 'b)
+val memo1_2 : ('a -> 'b -> 'c) -> ('a -> 'b -> 'c)
+(* with custom equality (used to deal with various arities) *)
+val memo1_eq : ('a -> 'a -> bool) -> ('a -> 'b) -> ('a -> 'b)
+
+(* Memorizes the last [n] distinct calls. Efficient only for small [n]. *)
+val memon_eq : ('a -> 'a -> bool) -> int -> ('a -> 'b) -> ('a -> 'b)
 
 (*s Size of an ocaml value (in words, bytes and kilobytes). *)
 
diff --git a/library/declaremods.ml b/library/declaremods.ml
index de1893c7..3026143b 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: declaremods.ml 11703 2008-12-18 15:54:41Z soubiran $ i*)
+(*i $Id: declaremods.ml 11898 2009-02-10 10:52:45Z soubiran $ i*)
 open Pp
 open Util
 open Names
@@ -628,6 +628,7 @@ let rec get_modtype_substobjs env = function
   | MSEwith (mty, With_Definition _) -> get_modtype_substobjs env mty
   | MSEwith (mty, With_Module (idl,mp)) -> 
       let substobjs = get_modtype_substobjs env mty in
+      let mp = Environ.scrape_alias mp env in
       let modobjs = MPmap.find mp !modtab_substobjs in
 	replace_module_object idl substobjs modobjs mp
   | MSEapply (mexpr, MSEident mp) ->
diff --git a/library/libnames.ml b/library/libnames.ml
index 3f226179..89a77128 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: libnames.ml 11750 2009-01-05 20:47:34Z herbelin $ i*)
+(*i $Id: libnames.ml 11878 2009-02-03 12:48:18Z soubiran $ i*)
 
 open Pp
 open Util
@@ -199,11 +199,23 @@ let encode_kn dir id = make_kn (MPfile dir) empty_dirpath (label_of_id id)
 let encode_con dir id = make_con (MPfile dir) empty_dirpath (label_of_id id)
 
 let decode_kn kn = 
+  let rec dir_of_mp = function
+    | MPfile dir -> repr_dirpath dir
+    | MPbound mbid -> 
+	let _,_,dp = repr_mbid mbid in
+	let id = id_of_mbid mbid in
+	  id::(repr_dirpath dp)
+    | MPself msid -> 
+	let _,_,dp = repr_msid msid in
+	let id = id_of_msid msid in
+	  id::(repr_dirpath dp) 
+    | MPdot(mp,l) -> (id_of_label l)::(dir_of_mp mp)
+  in
   let mp,sec_dir,l = repr_kn kn in
-    match mp,(repr_dirpath sec_dir) with
-	MPfile dir,[] -> (dir,id_of_label l)
-      | _ , [] -> anomaly "MPfile expected!"
-      | _ -> anomaly "Section part should be empty!"
+    if (repr_dirpath sec_dir) = [] then
+     (make_dirpath (dir_of_mp mp)),id_of_label l
+    else
+      anomaly "Section part should be empty!"
 
 let decode_con kn = 
   let mp,sec_dir,l = repr_con kn in
diff --git a/library/library.ml b/library/library.ml
index 9f3478f0..0e1342f0 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: library.ml 11801 2009-01-18 20:11:41Z herbelin $ *)
+(* $Id: library.ml 11897 2009-02-09 19:28:02Z barras $ *)
 
 open Pp
 open Util
@@ -629,6 +629,8 @@ let error_recursively_dependent_library dir =
      strbrk " to save current library because" ++
      strbrk " it already depends on a library of this name.")
 
+(* Security weakness: file might have been changed on disk between
+   writing the content and computing the checksum... *) 
 let save_library_to dir f =
   let cenv, seg = Declaremods.end_library dir in
   let md = { 
diff --git a/man/coqchk.1 b/man/coqchk.1
new file mode 100644
index 00000000..b0a9c6ab
--- /dev/null
+++ b/man/coqchk.1
@@ -0,0 +1,86 @@
+.TH COQ 1 "February 9, 2009"
+
+.SH NAME
+coqchk \- The Coq Proof Assistant compiled libraries verifier
+
+
+.SH SYNOPSIS
+.B coqchk
+[
+.B options
+]
+.I files-or-modules
+
+
+.SH DESCRIPTION
+
+.B coqchk
+is the standalone checker of compiled libraries (.vo files produced by
+coqc) for the Coq Proof Assistant. See the Reference Manual for more
+information. It returns with exit code 0 if all the requested tasks
+succeeded. A non-zero return code means that something went wrong: some
+library was not found, corrupted content, type-checking failure, etc.
+
+.IR files-or-modules \&
+is a list of modules to be checked. Modules can be referred to either
+by a filename (without the .vo suffix) or by their (possibly
+qualified) module name.
+
+.SH OPTIONS
+
+.TP
+.BI \-I \ dir, \ \-\-include \ dir
+add directory 
+.I dir
+in the include path
+
+.TP
+.BI \-R \ dir\ coqdir          
+recursively map physical
+.I dir
+to logical
+.I coqdir
+
+.TP
+.BI \-where
+print Coq's standard library location and exit
+
+.TP
+.BI \-silent
+makes coqchk less verbose.
+
+.TP
+.BI \-admit \ file-or-module
+tag the specified module and all its dependencies as trusted, and will
+not be rechecked, unless explicitely requested by other options.
+
+.TP
+.BI \-norec \ file-or-module
+specifies that the given module shall be verified without requesting
+to check its dependencies
+
+.TP
+.BI \-m,\ \-\-memory
+displays a summary of the memory used by the checker
+
+.TP
+.BI \-o,\ \-\-output\-context
+displays a summary of the logical content that have been
+verified: assumptions and usage of impredicativity
+
+.TP
+.BI \-impredicative\-set
+allows the checker to verify libraries that have been compiled with
+this flag.
+
+.SH SEE ALSO
+
+.BR coqtop (1),
+.BR coqc (1),
+.BR coq_makefile (1),
+.BR coqdep (1).
+.br
+.I
+The Coq Reference Manual.
+.I
+The Coq web site: http://coq.inria.fr
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 52b73535..a4880f5e 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: cases.ml 11708 2008-12-20 10:50:20Z msozeau $ *)
+(* $Id: cases.ml 11897 2009-02-09 19:28:02Z barras $ *)
 
 open Util
 open Names
@@ -981,7 +981,8 @@ let specialize_predicate newtomatchs (names,(depna,_)) cs tms ccl =
   let copti = if depna<>Anonymous then Some (build_dependent_constructor cs) else None in
   (* The substituends argsi, copti are all defined in gamma, x1...xn *)
   (* We need _parallel_ bindings to get gamma, x1...xn, tms |- ccl'' *)
-  let ccl'' = whd_betaiota (subst_predicate (argsi, copti) ccl' tms) in
+  let ccl'' =
+    whd_betaiota Evd.empty (subst_predicate (argsi, copti) ccl' tms) in
   (* We adjust ccl st: gamma, x1..xn, x1..xn, tms |- ccl'' *)
   let ccl''' = liftn_predicate n (n+1) ccl'' tms in
   (* We finally get gamma,x1..xn |- [X1,x1:=R1,x1]..[Xn,xn:=Rn,xn]pred'''*)
@@ -989,7 +990,8 @@ let specialize_predicate newtomatchs (names,(depna,_)) cs tms ccl =
 
 let find_predicate loc env evdref p current (IndType (indf,realargs)) dep tms =
   let pred= abstract_predicate env (evars_of !evdref) indf current dep tms p in
-  (pred, whd_betaiota (applist (pred, realargs@[current])), new_Type ())
+  (pred, whd_betaiota (evars_of !evdref)
+           (applist (pred, realargs@[current])), new_Type ())
 
 let adjust_predicate_from_tomatch ((_,oldtyp),_,(nadep,_)) typ pb =
   match typ, oldtyp with
@@ -1211,7 +1213,7 @@ and match_current pb tomatch =
 	    find_predicate pb.caseloc pb.env pb.evdref 
 	      pb.pred current indt (names,dep) pb.tomatch in
 	  let ci = make_case_info pb.env mind pb.casestyle in
-	  let case = mkCase (ci,nf_betaiota pred,current,brvals) in
+	  let case = mkCase (ci,nf_betaiota Evd.empty pred,current,brvals) in
 	  let inst = List.map mkRel deps in
 	  { uj_val = applist (case, inst);
 	    uj_type = substl inst typ }
@@ -1454,8 +1456,8 @@ let adjust_to_extended_env_and_remove_deps env extenv subst t =
 *)
 
 let abstract_tycon loc env evdref subst _tycon extenv t =
-  let t = nf_betaiota t in (* it helps in some cases to remove K-redex... *)
   let sigma = evars_of !evdref in
+  let t = nf_betaiota sigma t in (* it helps in some cases to remove K-redex *)
   let subst0,t0 = adjust_to_extended_env_and_remove_deps env extenv subst t in
   (* We traverse the type T of the original problem Xi looking for subterms
      that match the non-constructor part of the constraints (this part
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 2a01e901..f4c612a5 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: cbv.ml 8802 2006-05-10 20:47:28Z barras $ *)
+(* $Id: cbv.ml 11897 2009-02-09 19:28:02Z barras $ *)
 
 open Util
 open Pp
@@ -218,6 +218,11 @@ let rec norm_head info env t stack =
 		   cbv_norm_term info env' c) in
 	(VAL(0,normt), stack) (* Considérer une coupure commutative ? *)
 
+  | Evar ev ->
+      (match evar_value info ev with
+          Some c -> norm_head info env c stack
+        | None -> (VAL(0, t), stack))
+
   (* non-neutral cases *)
   | Lambda _ ->
       let ctxt,b = decompose_lam t in
@@ -227,7 +232,7 @@ let rec norm_head info env t stack =
   | Construct c -> (CONSTR(c, [||]), stack)
 
   (* neutral cases *)
-  | (Sort _ | Meta _ | Ind _|Evar _) -> (VAL(0, t), stack)
+  | (Sort _ | Meta _ | Ind _) -> (VAL(0, t), stack)
   | Prod (x,t,c) -> 
       (VAL(0, mkProd (x, cbv_norm_term info env t,
 		      cbv_norm_term info (subs_lift env) c)),
@@ -353,8 +358,9 @@ let cbv_norm infos constr =
 type cbv_infos = cbv_value infos
 
 (* constant bodies are normalized at the first expansion *)
-let create_cbv_infos flgs env =
+let create_cbv_infos flgs env sigma =
   create
     (fun old_info c -> cbv_stack_term old_info TOP (ESID 0) c)
     flgs
     env
+    (Reductionops.safe_evar_value sigma)
diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli
index 8c969e2c..9ab15886 100644
--- a/pretyping/cbv.mli
+++ b/pretyping/cbv.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: cbv.mli 8799 2006-05-09 21:15:07Z barras $ i*)
+(*i $Id: cbv.mli 11897 2009-02-09 19:28:02Z barras $ i*)
 
 (*i*)
 open Names
@@ -22,7 +22,7 @@ open Esubst
 (* Entry point for cbv normalization of a constr *)
 type cbv_infos
 
-val create_cbv_infos : RedFlags.reds -> env -> cbv_infos
+val create_cbv_infos : RedFlags.reds -> env -> Evd.evar_map -> cbv_infos
 val cbv_norm         : cbv_infos -> constr -> constr
 
 (************************************************************************)
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 398da529..27418b4d 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: classops.ml 11343 2008-09-01 20:55:13Z herbelin $ *)
+(* $Id: classops.ml 11897 2009-02-09 19:28:02Z barras $ *)
 
 open Util
 open Pp
@@ -143,7 +143,7 @@ let coercion_params coe_info = coe_info.coe_param
 (* find_class_type : env -> evar_map -> constr -> cl_typ * int *)
 
 let find_class_type env sigma t =
-  let t', args = Reductionops.whd_betaiotazetaevar_stack env sigma t in
+  let t', args = Reductionops.whd_betaiotazeta_stack sigma t in
   match kind_of_term t' with
     | Var id -> CL_SECVAR id, args
     | Const sp -> CL_CONST sp, args
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 8dfec2be..51952f4f 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: clenv.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: clenv.ml 11897 2009-02-09 19:28:02Z barras $ *)
 
 open Pp
 open Util
@@ -254,7 +254,7 @@ let clenv_unify_meta_types ?(flags=default_unify_flags) clenv =
   { clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd }
 
 let clenv_unique_resolver allow_K ?(flags=default_unify_flags) clenv gl =
-  if isMeta (fst (whd_stack clenv.templtyp.rebus)) then
+  if isMeta (fst (whd_stack (evars_of clenv.evd) clenv.templtyp.rebus)) then
     clenv_unify allow_K CUMUL ~flags:flags (clenv_type clenv) (pf_concl gl)
       (clenv_unify_meta_types ~flags:flags clenv)
   else
@@ -402,7 +402,7 @@ let error_already_defined b =
           (str "Position " ++ int n ++ str" already defined.")
 
 let clenv_unify_binding_type clenv c t u =
-  if isMeta (fst (whd_stack u)) then
+  if isMeta (fst (whd_stack (evars_of clenv.evd) u)) then
     (* Not enough information to know if some subtyping is needed *)
     CoerceToType, clenv, c
   else
@@ -416,7 +416,7 @@ let clenv_unify_binding_type clenv c t u =
 let clenv_assign_binding clenv k (sigma,c) =
   let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
   let clenv' = { clenv with evd = evar_merge clenv.evd sigma} in
-  let c_typ = nf_betaiota (clenv_get_type_of clenv' c) in
+  let c_typ = nf_betaiota (evars_of clenv'.evd) (clenv_get_type_of clenv' c) in
   let status,clenv'',c = clenv_unify_binding_type clenv' c c_typ k_typ in
   { clenv'' with evd = meta_assign k (c,(UserGiven,status)) clenv''.evd }
 
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 58369811..4c5ebe3e 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evarconv.ml 11745 2009-01-04 18:43:08Z herbelin $ *)
+(* $Id: evarconv.ml 11897 2009-02-09 19:28:02Z barras $ *)
 
 open Pp
 open Util
@@ -62,7 +62,7 @@ let evar_apprec env evd stack c =
   in aux (c, append_stack_list stack empty_stack)
 
 let apprec_nohdbeta env evd c =
-  match kind_of_term (fst (Reductionops.whd_stack c)) with
+  match kind_of_term (fst (Reductionops.whd_stack (evars_of evd) c)) with
     | (Case _ | Fix _) -> applist (evar_apprec env evd [] c)
     | _ -> c
 
@@ -164,18 +164,25 @@ let rec evar_conv_x env evd pbty term1 term2 =
   (* Maybe convertible but since reducing can erase evars which [evar_apprec]
      could have found, we do it only if the terms are free of evar.
      Note: incomplete heuristic... *)
-  if is_ground_term evd term1 && is_ground_term evd term2
-    && is_ground_env evd env
-  then (evd, is_fconv pbty env (evars_of evd) term1 term2)
-  else
-  let term1 = apprec_nohdbeta env evd term1 in
-  let term2 = apprec_nohdbeta env evd term2 in
-  if is_undefined_evar evd term1 then
-    solve_simple_eqn evar_conv_x env evd (pbty,destEvar term1,term2)
-  else if is_undefined_evar evd term2 then
-    solve_simple_eqn evar_conv_x env evd (pbty,destEvar term2,term1)
-  else
-    evar_eqappr_x env evd pbty (decompose_app term1) (decompose_app term2)
+  let ground_test =
+    if is_ground_term evd term1 && is_ground_term evd term2 then
+      if is_fconv pbty env (evars_of evd) term1 term2 then
+        Some true
+      else if is_ground_env evd env then Some false
+      else None
+    else None in
+  match ground_test with
+      Some b -> (evd,b)
+    | None ->
+        let term1 = apprec_nohdbeta env evd term1 in
+        let term2 = apprec_nohdbeta env evd term2 in
+        if is_undefined_evar evd term1 then
+          solve_simple_eqn evar_conv_x env evd (pbty,destEvar term1,term2)
+        else if is_undefined_evar evd term2 then
+          solve_simple_eqn evar_conv_x env evd (pbty,destEvar term2,term1)
+        else
+          evar_eqappr_x env evd pbty
+            (decompose_app term1) (decompose_app term2)
 
 and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
   (* Evar must be undefined since we have whd_ised *)
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index b418f996..c0c0b941 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evarutil.ml 11819 2009-01-20 20:04:50Z herbelin $ *)
+(* $Id: evarutil.ml 11897 2009-02-09 19:28:02Z barras $ *)
 
 open Util
 open Pp
@@ -119,7 +119,7 @@ let evars_to_metas sigma (emap, c) =
   let emap = nf_evars emap in
   let sigma',emap' = push_dependent_evars sigma emap in
   let change_exist evar =
-    let ty = nf_betaiota (nf_evar emap (existential_type emap evar)) in
+    let ty = nf_betaiota emap (existential_type emap evar) in
     let n = new_meta() in
     mkCast (mkMeta n, DEFAULTcast, ty) in
   let rec replace c =
@@ -906,7 +906,7 @@ let rec invert_definition env evd (evk,argsv as ev) rhs =
 	map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1)
 	  imitate envk t in
 
-  let rhs = whd_beta rhs (* heuristic *) in
+  let rhs = whd_beta (evars_of evd) rhs (* heuristic *) in
   let body = imitate (env,0) rhs in
   (!evdref,body)
 
@@ -959,9 +959,19 @@ and evar_define env (evk,_ as ev) rhs evd =
 (* Auxiliary functions for the conversion algorithms modulo evars
  *)
 
-let has_undefined_evars evd t = 
-  try let _ = local_strong (whd_ise (evars_of evd)) t in false
-  with Uninstantiated_evar _ -> true
+let has_undefined_evars evd t =
+  let evm = evars_of evd in
+  let rec has_ev t =
+    match kind_of_term t with
+        Evar (ev,args) ->
+          (match evar_body (Evd.find evm ev) with
+            | Evar_defined c ->
+                has_ev c; Array.iter has_ev args
+            | Evar_empty ->
+	        raise NotInstantiatedEvar)
+      | _ -> iter_constr has_ev t in
+  try let _ = has_ev t in false
+  with (Not_found | NotInstantiatedEvar) -> true
 
 let is_ground_term evd t =
   not (has_undefined_evars evd t)
@@ -972,6 +982,9 @@ let is_ground_env evd env =
     | _ -> true in
   List.for_all is_ground_decl (rel_context env) &&
   List.for_all is_ground_decl (named_context env)
+(* Memoization is safe since evar_map and environ are applicative
+   structures *)
+let is_ground_env = memo1_2 is_ground_env
 
 let head_evar = 
   let rec hrec c = match kind_of_term c with
@@ -1012,6 +1025,7 @@ let is_unification_pattern_evar env (_,args) l t =
 	    l
 	  else
 	    (* Probably strong restrictions coming from t being evar-closed *)
+	    let t = expand_vars_in_term env t in
 	    let fv_rels = free_rels t in
 	    let fv_ids = global_vars env t in
 	    List.filter (fun c ->
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index d3123eb6..88a0c2a6 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: indrec.ml 11735 2009-01-02 17:22:31Z herbelin $ *)
+(* $Id: indrec.ml 11897 2009-02-09 19:28:02Z barras $ *)
 
 open Pp
 open Util
@@ -229,7 +229,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
            | None ->
 	       lambda_name env
 		 (n,t,process_constr (push_rel d env) (i+1)
-		    (whd_beta (applist (lift 1 f, [(mkRel 1)])))
+		    (whd_beta Evd.empty (applist (lift 1 f, [(mkRel 1)])))
 		    (cprest,rest))
            | Some(_,f_0) -> 
 	       let nF = lift (i+1+decF) f_0 in
@@ -237,7 +237,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
 	       let arg = process_pos env' nF (lift 1 t) in 
                lambda_name env
 		 (n,t,process_constr env' (i+1)
-		    (whd_beta (applist (lift 1 f, [(mkRel 1); arg])))
+		    (whd_beta Evd.empty (applist (lift 1 f, [(mkRel 1); arg])))
 		    (cprest,rest)))
     | (n,Some c,t as d)::cprest, rest ->
 	mkLetIn
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index a1603d69..33928f67 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: reductionops.ml 11796 2009-01-18 13:41:39Z herbelin $ *)
+(* $Id: reductionops.ml 11897 2009-02-09 19:28:02Z barras $ *)
 
 open Pp
 open Util
@@ -114,31 +114,41 @@ type state = constr * constr stack
 
 type  contextual_reduction_function = env ->  evar_map -> constr -> constr
 type  reduction_function =  contextual_reduction_function
-type local_reduction_function = constr -> constr
+type local_reduction_function = evar_map -> constr -> constr
 
 type  contextual_stack_reduction_function = 
     env ->  evar_map -> constr -> constr * constr list
 type  stack_reduction_function =  contextual_stack_reduction_function
-type local_stack_reduction_function = constr -> constr * constr list
+type local_stack_reduction_function =
+    evar_map -> constr -> constr * constr list
 
 type  contextual_state_reduction_function = 
     env ->  evar_map -> state -> state
 type  state_reduction_function =  contextual_state_reduction_function
-type local_state_reduction_function = state -> state
+type local_state_reduction_function = evar_map -> state -> state
 
 (*************************************)
 (*** Reduction Functions Operators ***)
 (*************************************)
 
-let rec whd_state (x, stack as s) =
+let safe_evar_value sigma ev =
+  try Some (Evd.existential_value sigma ev)
+  with NotInstantiatedEvar | Not_found -> None
+
+let rec whd_state sigma (x, stack as s) =
   match kind_of_term x with
-    | App (f,cl) -> whd_state (f, append_stack cl stack)
-    | Cast (c,_,_)  -> whd_state (c, stack)
+    | App (f,cl) -> whd_state sigma (f, append_stack cl stack)
+    | Cast (c,_,_)  -> whd_state sigma (c, stack)
+    | Evar ev ->
+        (match safe_evar_value sigma ev with
+            Some c -> whd_state sigma (c,stack)
+          | _ -> s)
     | _             -> s
 
 let appterm_of_stack (f,s) = (f,list_of_stack s)
 
-let whd_stack x = appterm_of_stack (whd_state (x, empty_stack))
+let whd_stack sigma x =
+  appterm_of_stack (whd_state sigma (x, empty_stack))
 let whd_castapp_stack = whd_stack
 
 let stack_reduction_of_reduction red_fun env sigma s =
@@ -150,14 +160,14 @@ let strong whdfun env sigma t =
     map_constr_with_full_binders push_rel strongrec env (whdfun env sigma t) in
   strongrec env t
 
-let local_strong whdfun = 
-  let rec strongrec t = map_constr strongrec (whdfun t) in
+let local_strong whdfun sigma = 
+  let rec strongrec t = map_constr strongrec (whdfun sigma t) in
   strongrec
 
-let rec strong_prodspine redfun c = 
-  let x = redfun c in
+let rec strong_prodspine redfun sigma c = 
+  let x = redfun sigma c in
   match kind_of_term x with
-    | Prod (na,a,b) -> mkProd (na,a,strong_prodspine redfun b)
+    | Prod (na,a,b) -> mkProd (na,a,strong_prodspine redfun sigma b)
     | _ -> x
 
 (*************************************)
@@ -171,7 +181,6 @@ module type RedFlagsSig = sig
   type flags
   type flag
   val fbeta : flag
-  val fevar : flag
   val fdelta : flag
   val feta : flag
   val fiota : flag
@@ -179,7 +188,6 @@ module type RedFlagsSig = sig
   val mkflags : flag list -> flags
   val red_beta : flags -> bool
   val red_delta : flags -> bool
-  val red_evar : flags -> bool
   val red_eta : flags -> bool
   val red_iota : flags -> bool
   val red_zeta : flags -> bool
@@ -211,14 +219,12 @@ module RedFlags = (struct
   type flags = int
   let fbeta = 1
   let fdelta = 2
-  let fevar = 4
   let feta = 8 
   let fiota = 16
   let fzeta = 32
   let mkflags = List.fold_left (lor) 0
   let red_beta f = f land fbeta <> 0
   let red_delta f = f land fdelta <> 0
-  let red_evar f = f land fevar <> 0
   let red_eta f = f land feta <> 0
   let red_iota f = f land fiota <> 0
   let red_zeta f = f land fzeta <> 0
@@ -229,20 +235,16 @@ open RedFlags
 (* Local *)
 let beta = mkflags [fbeta]
 let eta = mkflags [feta]
-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]
-let betadelta = mkflags [fbeta;fdelta;fzeta;fevar]
-let betadeltaeta = mkflags [fbeta;fdelta;fzeta;fevar;feta]
-let betadeltaiota = mkflags [fbeta;fdelta;fzeta;fevar;fiota]
-let betadeltaiota_nolet = mkflags [fbeta;fdelta;fevar;fiota]
-let betadeltaiotaeta = mkflags [fbeta;fdelta;fzeta;fevar;fiota;feta]
-let betaiotaevar = mkflags [fbeta;fiota;fevar]
+let delta = mkflags [fdelta]
+let betadelta = mkflags [fbeta;fdelta;fzeta]
+let betadeltaeta = mkflags [fbeta;fdelta;fzeta;feta]
+let betadeltaiota = mkflags [fbeta;fdelta;fzeta;fiota]
+let betadeltaiota_nolet = mkflags [fbeta;fdelta;fiota]
+let betadeltaiotaeta = mkflags [fbeta;fdelta;fzeta;fiota;feta]
 let betaetalet = mkflags [fbeta;feta;fzeta]
 let betalet = mkflags [fbeta;fzeta]
 
@@ -303,11 +305,11 @@ let fix_recarg ((recindices,bodynum),_) stack =
 
 type fix_reduction_result = NotReducible | Reduced of state
 
-let reduce_fix whdfun fix stack =
+let reduce_fix whdfun sigma fix stack =
   match fix_recarg fix stack with
     | None -> NotReducible
     | Some (recargnum,recarg) ->
-        let (recarg'hd,_ as recarg') = whdfun (recarg, empty_stack) in
+        let (recarg'hd,_ as recarg') = whdfun sigma (recarg, empty_stack) in
         let stack' = stack_assign stack recargnum (app_stack recarg') in
 	(match kind_of_term recarg'hd with
            | Construct _ -> Reduced (contract_fix fix, stack')
@@ -333,8 +335,8 @@ let rec whd_state_gen flags env sigma =
 	  (match lookup_named id env with
 	     | (_,Some body,_) -> whrec (body, stack)
 	     | _ -> s)
-      | Evar ev when red_evar flags ->
-	  (match existential_opt_value sigma ev with
+      | Evar ev ->
+	  (match safe_evar_value sigma ev with
 	     | Some body -> whrec (body, stack)
 	     | None -> s)
       | Const const when red_delta flags ->
@@ -375,7 +377,7 @@ let rec whd_state_gen flags env sigma =
 	    (mkCase (ci, p, app_stack (c,cargs), lf), stack)
             
       | Fix fix when red_iota flags ->
-	  (match reduce_fix whrec fix stack with
+	  (match reduce_fix (fun _ -> whrec) sigma fix stack with
              | Reduced s' -> whrec s'
 	     | NotReducible -> s)
 
@@ -383,7 +385,7 @@ let rec whd_state_gen flags env sigma =
   in 
   whrec
 
-let local_whd_state_gen flags = 
+let local_whd_state_gen flags sigma = 
   let rec whrec (x, stack as s) =
     match kind_of_term x with
       | LetIn (_,b,_,c) when red_zeta flags -> stacklam whrec [b] c stack
@@ -418,105 +420,91 @@ let local_whd_state_gen flags =
 	    (mkCase (ci, p, app_stack (c,cargs), lf), stack)
             
       | Fix fix when red_iota flags ->
-	  (match reduce_fix whrec fix stack with
+	  (match reduce_fix (fun _ ->whrec) sigma fix stack with
              | Reduced s' -> whrec s'
 	     | NotReducible -> s)
 
+      | Evar ev ->
+          (match safe_evar_value sigma ev with
+              Some c -> whrec (c,stack)
+            | None -> s)
+
       | x -> s
   in 
   whrec
 
 
+let stack_red_of_state_red f sigma x =
+  appterm_of_stack (f sigma (x, empty_stack))
+
+let red_of_state_red f sigma x =
+  app_stack (f sigma (x,empty_stack))
+
 (* 1. Beta Reduction Functions *)
 
 let whd_beta_state = local_whd_state_gen beta
-let whd_beta_stack x = appterm_of_stack (whd_beta_state (x, empty_stack))
-let whd_beta x = app_stack (whd_beta_state (x,empty_stack))
+let whd_beta_stack = stack_red_of_state_red whd_beta_state
+let whd_beta = red_of_state_red whd_beta_state
 
 (* Nouveau ! *)
 let whd_betaetalet_state = local_whd_state_gen betaetalet
-let whd_betaetalet_stack x =
-  appterm_of_stack (whd_betaetalet_state (x, empty_stack))
-let whd_betaetalet x = app_stack (whd_betaetalet_state (x,empty_stack))
+let whd_betaetalet_stack = stack_red_of_state_red whd_betaetalet_state
+let whd_betaetalet = red_of_state_red whd_betaetalet_state
 
 let whd_betalet_state = local_whd_state_gen betalet
-let whd_betalet_stack x = appterm_of_stack (whd_betalet_state (x, empty_stack))
-let whd_betalet x = app_stack (whd_betalet_state (x,empty_stack))
+let whd_betalet_stack = stack_red_of_state_red whd_betalet_state
+let whd_betalet = red_of_state_red whd_betalet_state
 
 (* 2. Delta Reduction Functions *)
 
 let whd_delta_state e = whd_state_gen delta e
-let whd_delta_stack env sigma x =
-  appterm_of_stack (whd_delta_state env sigma (x, empty_stack))
-let whd_delta env sigma c =
-  app_stack (whd_delta_state env sigma (c, empty_stack))
+let whd_delta_stack env = stack_red_of_state_red (whd_delta_state env)
+let whd_delta env = red_of_state_red  (whd_delta_state env)
 
 let whd_betadelta_state e = whd_state_gen betadelta e
-let whd_betadelta_stack env sigma x =
-  appterm_of_stack (whd_betadelta_state env sigma (x, empty_stack))
-let whd_betadelta env sigma c =
-  app_stack (whd_betadelta_state env sigma (c, empty_stack))
-
-let whd_betaevar_state e = whd_state_gen betaevar e
-let whd_betaevar_stack env sigma c =
-  appterm_of_stack (whd_betaevar_state env sigma (c, empty_stack))
-let whd_betaevar env sigma c =
-  app_stack (whd_betaevar_state env sigma (c, empty_stack))
+let whd_betadelta_stack env =
+  stack_red_of_state_red (whd_betadelta_state env)
+let whd_betadelta env =
+  red_of_state_red (whd_betadelta_state env)
 
 
 let whd_betadeltaeta_state e = whd_state_gen betadeltaeta e
-let whd_betadeltaeta_stack env sigma x =
-  appterm_of_stack (whd_betadeltaeta_state env sigma (x, empty_stack))
-let whd_betadeltaeta env sigma x = 
-  app_stack (whd_betadeltaeta_state env sigma (x, empty_stack))
+let whd_betadeltaeta_stack env =
+  stack_red_of_state_red (whd_betadeltaeta_state env)
+let whd_betadeltaeta env = 
+  red_of_state_red (whd_betadeltaeta_state env)
 
 (* 3. Iota reduction Functions *)
 
 let whd_betaiota_state = local_whd_state_gen betaiota
-let whd_betaiota_stack x =
-  appterm_of_stack (whd_betaiota_state (x, empty_stack))
-let whd_betaiota x =
-  app_stack (whd_betaiota_state (x, empty_stack))
+let whd_betaiota_stack = stack_red_of_state_red whd_betaiota_state
+let whd_betaiota = red_of_state_red whd_betaiota_state
 
 let whd_betaiotazeta_state = local_whd_state_gen betaiotazeta
-let whd_betaiotazeta_stack x =
-  appterm_of_stack (whd_betaiotazeta_state (x, empty_stack))
-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))
-let whd_betaiotaevar env sigma x = 
-  app_stack (whd_betaiotaevar_state env sigma (x, empty_stack))
+let whd_betaiotazeta_stack = stack_red_of_state_red whd_betaiotazeta_state
+let whd_betaiotazeta = red_of_state_red whd_betaiotazeta_state
 
 let whd_betadeltaiota_state e = whd_state_gen betadeltaiota e
-let whd_betadeltaiota_stack env sigma x =
-  appterm_of_stack (whd_betadeltaiota_state env sigma (x, empty_stack))
-let whd_betadeltaiota env sigma x = 
-  app_stack (whd_betadeltaiota_state env sigma (x, empty_stack))
+let whd_betadeltaiota_stack env =
+  stack_red_of_state_red (whd_betadeltaiota_state env)
+let whd_betadeltaiota env = 
+  red_of_state_red (whd_betadeltaiota_state env)
 
 let whd_betadeltaiotaeta_state e = whd_state_gen betadeltaiotaeta e
-let whd_betadeltaiotaeta_stack env sigma x =
-  appterm_of_stack (whd_betadeltaiotaeta_state env sigma (x, empty_stack))
-let whd_betadeltaiotaeta env sigma x = 
-  app_stack (whd_betadeltaiotaeta_state env sigma (x, empty_stack))
+let whd_betadeltaiotaeta_stack env =
+  stack_red_of_state_red (whd_betadeltaiotaeta_state env)
+let whd_betadeltaiotaeta env = 
+  red_of_state_red (whd_betadeltaiotaeta_state env)
 
 let whd_betadeltaiota_nolet_state e = whd_state_gen betadeltaiota_nolet e
-let whd_betadeltaiota_nolet_stack env sigma x =
-  appterm_of_stack (whd_betadeltaiota_nolet_state env sigma (x, empty_stack))
-let whd_betadeltaiota_nolet env sigma x = 
-  app_stack (whd_betadeltaiota_nolet_state env sigma (x, empty_stack))
+let whd_betadeltaiota_nolet_stack env =
+  stack_red_of_state_red (whd_betadeltaiota_nolet_state env)
+let whd_betadeltaiota_nolet env = 
+  red_of_state_red (whd_betadeltaiota_nolet_state env)
 
 (* 3. Eta reduction Functions *)
 
-let whd_eta c = app_stack (local_whd_state_gen eta (c,empty_stack))
+let whd_eta c = app_stack (local_whd_state_gen eta Evd.empty (c,empty_stack))
 
 (****************************************************************************)
 (*                   Reduction Functions                                    *)
@@ -526,24 +514,25 @@ let whd_eta c = app_stack (local_whd_state_gen eta (c,empty_stack))
 let rec whd_evar sigma c =
   match kind_of_term c with
     | Evar ev ->
-	let d = 
-	  try Some (Evd.existential_value sigma ev)
-	  with NotInstantiatedEvar | Not_found -> None in
-	(match d with Some c -> whd_evar sigma c | None -> c)
+        (match safe_evar_value sigma ev with
+            Some c -> whd_evar sigma c
+          | None -> c)
     | Sort s when is_sort_variable sigma s -> whd_sort_variable sigma c
     | _ -> collapse_appl c
 
-let nf_evar sigma =
-  local_strong (whd_evar sigma)
+let nf_evar =
+  local_strong whd_evar
 
 (* lazy reduction functions. The infos must be created for each term *)
 (* Note by HH [oct 08] : why would it be the job of clos_norm_flags to add
    a [nf_evar] here *)
 let clos_norm_flags flgs env sigma t =
-  norm_val (create_clos_infos flgs env) (inject (nf_evar sigma t))
+  norm_val
+    (create_clos_infos ~evars:(safe_evar_value sigma) flgs env)
+    (inject t)
 
-let nf_beta = clos_norm_flags Closure.beta empty_env Evd.empty
-let nf_betaiota = clos_norm_flags Closure.betaiota empty_env Evd.empty
+let nf_beta = clos_norm_flags Closure.beta empty_env
+let nf_betaiota = clos_norm_flags Closure.betaiota empty_env
 let nf_betadeltaiota env sigma =
   clos_norm_flags Closure.betadeltaiota env sigma
 
@@ -553,7 +542,7 @@ let nf_betadeltaiota env sigma =
    du type checking :
      (fun x => x + x) M
 *)
-let rec whd_betaiotaevar_preserving_vm_cast env sigma t = 	 
+let rec whd_betaiota_preserving_vm_cast env sigma t = 	 
    let rec stacklam_var subst t stack = 	 
      match (decomp_stack stack,kind_of_term t) with 	 
      | Some (h,stacktl), Lambda (_,_,c) -> 	 
@@ -568,7 +557,7 @@ let rec whd_betaiotaevar_preserving_vm_cast env sigma t =
    and whrec (x, stack as s) = 	 
      match kind_of_term x with 	 
        | Evar ev -> 	 
-           (match existential_opt_value sigma ev with 	 
+           (match safe_evar_value sigma ev with 	 
               | Some body -> whrec (body, stack) 	 
               | None -> s) 	 
        | Cast (c,VMcast,t) -> 	 
@@ -594,12 +583,14 @@ let rec whd_betaiotaevar_preserving_vm_cast env sigma t =
    in 	 
    app_stack (whrec (t,empty_stack))
 
-let nf_betaiotaevar_preserving_vm_cast = 
-  strong whd_betaiotaevar_preserving_vm_cast
+let nf_betaiota_preserving_vm_cast = 
+  strong whd_betaiota_preserving_vm_cast
 
 (* lazy weak head reduction functions *)
 let whd_flags flgs env sigma t =
-  whd_val (create_clos_infos flgs env) (inject (nf_evar sigma t))
+  whd_val
+    (create_clos_infos ~evars:(safe_evar_value sigma) flgs env)
+    (inject t)
 
 (********************************************************************)
 (*                         Conversion                               *)
@@ -627,23 +618,9 @@ let pb_equal = function
 
 let sort_cmp = sort_cmp
 
-
-let nf_red_env sigma env =
-  let nf_decl = function
-      (x,Some t,ty) -> (x,Some (nf_evar sigma t),ty)
-    | d -> d in
-  let sign = named_context env in
-  let ctxt = rel_context env in
-  let env = reset_context env in
-  let env = Sign.fold_named_context
-    (fun d env -> push_named (nf_decl d) env) ~init:env sign in
-  Sign.fold_rel_context
-    (fun d env -> push_rel (nf_decl d) env) ~init:env ctxt
-
-
-let test_conversion f env sigma x y =
+let test_conversion (f:?evars:'a->'b) env sigma x y =
   try let _ =
-    f (nf_red_env sigma env) (nf_evar sigma x) (nf_evar sigma y) in true
+    f ~evars:(safe_evar_value sigma) env x y in true
   with NotConvertible -> false
 
 let is_conv env sigma = test_conversion Reduction.conv env sigma
@@ -729,7 +706,8 @@ let plain_instance s c =
  *)
 
 let instance s c =
-  (* if s = [] then c else *) local_strong whd_betaiota (plain_instance s c)
+  (* if s = [] then c else *)
+  local_strong whd_betaiota Evd.empty (plain_instance s c)
 
 (* pseudo-reduction rule:
  * [hnf_prod_app env s (Prod(_,B)) N --> B[N]
@@ -830,7 +808,7 @@ let is_sort env sigma arity =
 
 let whd_betaiota_deltazeta_for_iota_state env sigma s =
   let rec whrec s = 
-    let (t, stack as s) = whd_betaiota_state s in
+    let (t, stack as s) = whd_betaiota_state sigma s in
     match kind_of_term t with
     | Case (ci,p,d,lf) ->
         let (cr,crargs) = whd_betadeltaiota_stack env sigma d in
@@ -840,7 +818,7 @@ let whd_betaiota_deltazeta_for_iota_state env sigma s =
         else 
 	  s
     | Fix fix ->
-	  (match reduce_fix (whd_betadeltaiota_state env sigma) fix stack with
+	  (match reduce_fix (whd_betadeltaiota_state env) sigma fix stack with
              | Reduced s -> whrec s
 	     | NotReducible -> s)
     | _ -> s
@@ -882,7 +860,7 @@ let whd_programs_stack env sigma =
 	    else
 	      (mkCase (ci, p, app_stack(c,cargs), lf), stack)
       | Fix fix ->
-	  (match reduce_fix whrec fix stack with
+	  (match reduce_fix (fun _ ->whrec) sigma  fix stack with
              | Reduced s' -> whrec s'
 	     | NotReducible -> s)
       | _ -> s
@@ -952,7 +930,7 @@ let meta_reducible_instance evd b =
     | Some (g,(_,s)) -> (mv,(g.rebus,s))::l 
     | None -> l) [] fm in
   let rec irec u =
-    let u = whd_betaiota u in
+    let u = whd_betaiota Evd.empty u in
     match kind_of_term u with
     | Case (ci,p,c,bl) when isMeta c or isCast c & isMeta (pi1 (destCast c)) ->
 	let m = try destMeta c with _ -> destMeta (pi1 (destCast c)) in
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index c026d9fe..8b3657c7 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 11343 2008-09-01 20:55:13Z herbelin $ i*)
+(*i $Id: reductionops.mli 11897 2009-02-09 19:28:02Z barras $ i*)
 
 (*i*)
 open Names
@@ -54,17 +54,18 @@ type state = constr * constr stack
 
 type contextual_reduction_function = env -> evar_map -> constr -> constr
 type reduction_function = contextual_reduction_function
-type local_reduction_function = constr -> constr
+type local_reduction_function = evar_map -> constr -> constr
 
 type contextual_stack_reduction_function = 
     env -> evar_map -> constr -> constr * constr list
 type stack_reduction_function = contextual_stack_reduction_function
-type local_stack_reduction_function = constr -> constr * constr list
+type local_stack_reduction_function =
+    evar_map -> constr -> constr * constr list
 
 type contextual_state_reduction_function = 
     env -> evar_map -> state -> state
 type state_reduction_function = contextual_state_reduction_function
-type local_state_reduction_function = state -> state
+type local_state_reduction_function = evar_map -> state -> state
 
 (* Removes cast and put into applicative form *)
 val whd_stack : local_stack_reduction_function
@@ -92,13 +93,12 @@ val nf_betaiota : local_reduction_function
 val nf_betadeltaiota : reduction_function
 val nf_evar : evar_map -> constr -> constr
 
-val nf_betaiotaevar_preserving_vm_cast : reduction_function
+val nf_betaiota_preserving_vm_cast : reduction_function
 (* Lazy strategy, weak head reduction *)
 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
@@ -106,7 +106,7 @@ val whd_betalet : local_reduction_function
 
 val whd_beta_stack : local_stack_reduction_function
 val whd_betaiota_stack : local_stack_reduction_function
-val whd_betaiotazetaevar_stack : contextual_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_betaetalet_stack : local_stack_reduction_function
@@ -114,7 +114,7 @@ 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_betaiotazetaevar_state : contextual_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_betaetalet_state : local_state_reduction_function
@@ -128,12 +128,6 @@ val whd_delta :  reduction_function
 val whd_betadelta_stack :  stack_reduction_function
 val whd_betadelta_state :  state_reduction_function
 val whd_betadelta :  reduction_function
-val whd_betaevar_stack :  stack_reduction_function
-val whd_betaevar_state :  state_reduction_function
-val whd_betaevar :  reduction_function
-val whd_betaiotaevar_stack :  stack_reduction_function
-val whd_betaiotaevar_state :  state_reduction_function
-val whd_betaiotaevar :  reduction_function
 val whd_betadeltaeta_stack :  stack_reduction_function
 val whd_betadeltaeta_state :  state_reduction_function
 val whd_betadeltaeta :  reduction_function
@@ -143,8 +137,9 @@ val whd_betadeltaiotaeta :  reduction_function
 
 val whd_eta : constr -> constr
 
+(* Various reduction functions *)
 
-
+val safe_evar_value : evar_map -> existential -> constr option
 
 val beta_applist : constr * constr list -> constr
 
@@ -187,7 +182,7 @@ val whd_programs :  reduction_function
 type fix_reduction_result = NotReducible | Reduced of state
 
 val fix_recarg : fixpoint -> constr stack -> (int * constr) option
-val reduce_fix : local_state_reduction_function -> fixpoint
+val reduce_fix : local_state_reduction_function -> evar_map -> fixpoint
    -> constr stack -> fix_reduction_result
 
 (*s Querying the kernel conversion oracle: opaque/transparent constants *)
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 2465bd1e..19e46a47 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: retyping.ml 11778 2009-01-13 13:17:39Z msozeau $ *)
+(* $Id: retyping.ml 11897 2009-02-09 19:28:02Z barras $ *)
 
 open Util
 open Term
@@ -62,9 +62,9 @@ let retype sigma metamap =
         let Inductiveops.IndType(_,realargs) =
           try Inductiveops.find_rectype env sigma (type_of env c)
           with Not_found -> anomaly "type_of: Bad recursive type" in
-        let t = whd_beta (applist (p, realargs)) in
+        let t = whd_beta sigma (applist (p, realargs)) in
         (match kind_of_term (whd_betadeltaiota env sigma (type_of env t)) with
-          | Prod _ -> whd_beta (applist (t, [c]))
+          | Prod _ -> whd_beta sigma (applist (t, [c]))
           | _ -> t)
     | Lambda (name,c1,c2) ->
           mkProd (name, c1, type_of (push_rel (name,None,c1) env) c2)
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 88a6f499..740b2ca8 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tacred.ml 11654 2008-12-03 18:39:40Z barras $ *)
+(* $Id: tacred.ml 11897 2009-02-09 19:28:02Z barras $ *)
 
 open Pp
 open Util
@@ -204,7 +204,7 @@ let invert_name labs l na0 env sigma ref = function
 		| None -> None
 		| Some c -> 
 		    let labs',ccl = decompose_lam c in
-		    let _, l' = whd_betalet_stack ccl in
+		    let _, l' = whd_betalet_stack sigma ccl in
 		    let labs' = List.map snd labs' in
 		    if labs' = labs & l = l' then Some (minfxargs,ref)
                     else None
@@ -234,7 +234,7 @@ let compute_consteval_direct sigma env ref =
 
 let compute_consteval_mutual_fix sigma env ref =
   let rec srec env minarg labs ref c =
-    let c',l = whd_betalet_stack c in
+    let c',l = whd_betalet_stack sigma c in
     let nargs = List.length l in
     match kind_of_term c' with
       | Lambda (na,t,g) when l=[] ->
@@ -378,7 +378,7 @@ let solve_arity_problem env sigma fxminargs c =
   let evm = ref sigma in
   let set_fix i = evm := Evd.define !evm i (mkVar vfx) in
   let rec check strict c =
-    let c' = whd_betaiotazeta c in
+    let c' = whd_betaiotazeta sigma c in
     let (h,rcargs) = decompose_app c' in
     match kind_of_term h with
         Evar(i,_) when Intmap.mem i fxminargs && not (Evd.is_defined !evm i) ->
@@ -418,14 +418,14 @@ let substl_checking_arity env subst c =
 
 
 
-let contract_fix_use_function env f
+let contract_fix_use_function env sigma f
   ((recindices,bodynum),(_names,_types,bodies as typedbodies)) =
   let nbodies = Array.length recindices in
   let make_Fi j = (mkFix((recindices,j),typedbodies), f j) in
   let lbodies = list_tabulate make_Fi nbodies in
-  substl_checking_arity env (List.rev lbodies) (nf_beta bodies.(bodynum))
+  substl_checking_arity env (List.rev lbodies) (nf_beta sigma bodies.(bodynum))
 
-let reduce_fix_use_function env f whfun fix stack =
+let reduce_fix_use_function env sigma f whfun fix stack =
   match fix_recarg fix stack with
     | None -> NotReducible
     | Some (recargnum,recarg) ->
@@ -438,17 +438,18 @@ let reduce_fix_use_function env f whfun fix stack =
         let stack' = stack_assign stack recargnum (app_stack recarg') in
 	(match kind_of_term recarg'hd with
            | Construct _ ->
-	       Reduced (contract_fix_use_function env f fix,stack')
+	       Reduced (contract_fix_use_function env sigma f fix,stack')
 	   | _ -> NotReducible)
 
-let contract_cofix_use_function env f
+let contract_cofix_use_function env sigma f
   (bodynum,(_names,_,bodies as typedbodies)) =
   let nbodies = Array.length bodies in
   let make_Fi j = (mkCoFix(j,typedbodies), f j) in
   let subbodies = list_tabulate make_Fi nbodies in
-  substl_checking_arity env (List.rev subbodies) (nf_beta bodies.(bodynum))
+  substl_checking_arity env (List.rev subbodies)
+    (nf_beta sigma bodies.(bodynum))
 
-let reduce_mind_case_use_function func env mia =
+let reduce_mind_case_use_function func env sigma mia =
   match kind_of_term mia.mconstr with 
     | Construct(ind_sp,i) ->
 	let real_cargs = list_skipn mia.mci.ci_npar mia.mcargs in
@@ -476,11 +477,11 @@ let reduce_mind_case_use_function func env mia =
 	  else
 	    fun _ -> None in
 	let cofix_def =
-          contract_cofix_use_function env build_cofix_name cofix in
+          contract_cofix_use_function env sigma build_cofix_name cofix in
 	mkCase (mia.mci, mia.mP, applist(cofix_def,mia.mcargs), mia.mlf)
     | _ -> assert false
 
-let special_red_case sigma env whfun (ci, p, c, lf)  =
+let special_red_case env sigma whfun (ci, p, c, lf)  =
   let rec redrec s = 
     let (constr, cargs) = whfun s in 
     if isEvalRef env constr then
@@ -489,7 +490,7 @@ let special_red_case sigma env whfun (ci, p, c, lf)  =
         | None -> raise Redelimination
         | Some gvalue ->
 	    if reducible_mind_case gvalue then
-	      reduce_mind_case_use_function constr env
+	      reduce_mind_case_use_function constr env sigma
 	        {mP=p; mconstr=gvalue; mcargs=list_of_stack cargs;
                 mci=ci; mlf=lf}
 	    else
@@ -514,15 +515,15 @@ let rec red_elim_const env sigma ref largs =
 	let c = reference_value sigma env ref in
 	let c', lrest = whd_betadelta_state env sigma (c,largs) in
 	let whfun = whd_simpl_state env sigma in
-        (special_red_case sigma env whfun (destCase c'), lrest)
+        (special_red_case env sigma whfun (destCase c'), lrest)
     | EliminationFix (min,minfxargs,infos) when stack_args_size largs >=min ->
 	let c = reference_value sigma env ref in
 	let d, lrest = whd_betadelta_state env sigma (c,largs) in
 	let f = make_elim_fun ([|Some (minfxargs,ref)|],infos) largs in
 	let whfun = whd_construct_state env sigma in
-	(match reduce_fix_use_function env f whfun (destFix d) lrest with
+	(match reduce_fix_use_function env sigma f whfun (destFix d) lrest with
 	   | NotReducible -> raise Redelimination
-	   | Reduced (c,rest) -> (nf_beta c, rest))
+	   | Reduced (c,rest) -> (nf_beta sigma c, rest))
     | EliminationMutualFix (min,refgoal,refinfos)
 	when stack_args_size largs >= min ->
 	let rec descend ref args =
@@ -530,15 +531,15 @@ let rec red_elim_const env sigma ref largs =
 	  if ref = refgoal then
 	    (c,args)
 	  else
-	    let c', lrest = whd_betalet_state (c,args) in
+	    let c', lrest = whd_betalet_state sigma (c,args) in
 	    descend (destEvalRef c') lrest in
 	let (_, midargs as s) = descend ref largs in
 	let d, lrest = whd_betadelta_state env sigma s in
 	let f = make_elim_fun refinfos midargs in
 	let whfun = whd_construct_state env sigma in
-	(match reduce_fix_use_function env f whfun (destFix d) lrest with
+	(match reduce_fix_use_function env sigma f whfun (destFix d) lrest with
 	   | NotReducible -> raise Redelimination
-	   | Reduced (c,rest) -> (nf_beta c, rest))
+	   | Reduced (c,rest) -> (nf_beta sigma c, rest))
     | _ -> raise Redelimination
 
 (* reduce to whd normal form or to an applied constant that does not hide
@@ -556,11 +557,11 @@ and whd_simpl_state env sigma s =
       | Cast (c,_,_) -> redrec (c, stack)
       | Case (ci,p,c,lf) ->
           (try 
-	    redrec (special_red_case sigma env redrec (ci,p,c,lf), stack)
+	    redrec (special_red_case env sigma redrec (ci,p,c,lf), stack)
 	  with
 	      Redelimination -> s)
       | Fix fix ->
-	  (try match reduce_fix (whd_construct_state env sigma) fix stack with
+	  (try match reduce_fix (whd_construct_state env) sigma fix stack with
             | Reduced s' -> redrec s'
 	    | NotReducible -> s
 	  with Redelimination -> s)
@@ -660,7 +661,7 @@ let whd_simpl_orelse_delta_but_fix_old env sigma c =
       | Cast (c,_,_) -> redrec (c, stack)
       | Case (ci,p,d,lf) ->
           (try
-             redrec (special_red_case sigma env whd_all (ci,p,d,lf), stack)
+             redrec (special_red_case env sigma whd_all (ci,p,d,lf), stack)
            with Redelimination -> 
 	     s)
       | Fix fix ->
@@ -795,7 +796,7 @@ let unfoldoccs env sigma ((nowhere_except_in,locs as plocs),name) c =
       error ((string_of_evaluable_ref env name)^" does not occur.");
     let rest = List.filter (fun o -> o >= nbocc) locs in
     if rest <> [] then error_invalid_occurrence rest;
-    nf_betaiota uc
+    nf_betaiota sigma uc
 
 (* Unfold reduction tactic: *)
 let unfoldn loccname env sigma c = 
@@ -824,10 +825,10 @@ let fold_commands cl env sigma c =
 
 (* call by value reduction functions *)
 let cbv_norm_flags flags env sigma t =
-  cbv_norm (create_cbv_infos flags env) (nf_evar sigma t)
+  cbv_norm (create_cbv_infos flags env sigma) t
 
-let cbv_beta = cbv_norm_flags beta empty_env Evd.empty
-let cbv_betaiota = cbv_norm_flags betaiota empty_env Evd.empty
+let cbv_beta = cbv_norm_flags beta empty_env
+let cbv_betaiota = cbv_norm_flags betaiota empty_env
 let cbv_betadeltaiota env sigma =  cbv_norm_flags betadeltaiota env sigma
 
 let compute = cbv_betadeltaiota
@@ -899,11 +900,11 @@ let one_step_reduce env sigma c =
       | Cast (c,_,_) -> redrec (c,stack)
       | Case (ci,p,c,lf) ->
           (try
-	     (special_red_case sigma env (whd_simpl_state env sigma)
+	     (special_red_case env sigma (whd_simpl_state env sigma)
 	       (ci,p,c,lf), stack)
            with Redelimination -> raise NotStepReducible)
       | Fix fix ->
-	  (match reduce_fix (whd_construct_state env sigma) fix stack with
+	  (match reduce_fix (whd_construct_state env) sigma fix stack with
              | Reduced s' -> s'
 	     | NotReducible -> raise NotStepReducible)
       | _ when isEvalRef env x ->
@@ -932,7 +933,7 @@ let reduce_to_ref_gen allow_product env sigma ref t =
   else
   (* lazily reduces to match the head of [t] with the expected [ref] *)
   let rec elimrec env t l = 
-    let c, _ = Reductionops.whd_stack t in
+    let c, _ = Reductionops.whd_stack sigma t in
     match kind_of_term c with
       | Prod (n,ty,t') ->
 	  if allow_product then
@@ -948,7 +949,7 @@ let reduce_to_ref_gen allow_product env sigma ref t =
 	    else raise Not_found
 	  with Not_found ->
           try 
-	    let t' = nf_betaiota (one_step_reduce env sigma t) in 
+	    let t' = nf_betaiota sigma (one_step_reduce env sigma t) in 
 	    elimrec env t' l
           with NotStepReducible ->
 	    errorlabstrm ""
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 981a5605..fb29196c 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: unification.ml 11819 2009-01-20 20:04:50Z herbelin $ *)
+(* $Id: unification.ml 11897 2009-02-09 19:28:02Z barras $ *)
 
 open Pp
 open Util
@@ -268,21 +268,25 @@ let unify_0_with_initial_metas subst conv_at_top env sigma cv_pb flags m n =
 	| Some true -> 
 	    (match expand_key curenv cf1 with
 	    | Some c ->
-		unirec_rec curenvnb pb b substn (whd_betaiotazeta (mkApp(c,l1))) cN
+		unirec_rec curenvnb pb b substn
+                  (whd_betaiotazeta sigma (mkApp(c,l1))) cN
 	    | None ->
 		(match expand_key curenv cf2 with
 		| Some c ->
-		    unirec_rec curenvnb pb b substn cM (whd_betaiotazeta (mkApp(c,l2)))
+		    unirec_rec curenvnb pb b substn cM
+                      (whd_betaiotazeta sigma (mkApp(c,l2)))
 		| None ->
 		    error_cannot_unify curenv sigma (cM,cN)))
 	| Some false ->
 	    (match expand_key curenv cf2 with
 	    | Some c ->
-		unirec_rec curenvnb pb b substn cM (whd_betaiotazeta (mkApp(c,l2)))
+		unirec_rec curenvnb pb b substn cM
+                  (whd_betaiotazeta sigma (mkApp(c,l2)))
 	    | None ->
 		(match expand_key curenv cf1 with
 		| Some c ->
-		    unirec_rec curenvnb pb b substn (whd_betaiotazeta (mkApp(c,l1))) cN
+		    unirec_rec curenvnb pb b substn
+                      (whd_betaiotazeta sigma (mkApp(c,l1))) cN
 		| None ->
 		    error_cannot_unify curenv sigma (cM,cN)))
     else
@@ -489,7 +493,7 @@ let unify_to_type env evd flags c u =
   let sigma = evars_of evd in
   let c = refresh_universes c in
   let t = get_type_of_with_meta env sigma (metas_of evd) c in
-  let t = Tacred.hnf_constr env sigma (nf_betaiota (nf_meta evd t)) in
+  let t = Tacred.hnf_constr env sigma (nf_betaiota sigma (nf_meta evd t)) in
   let u = Tacred.hnf_constr env sigma u in
   try unify_0 env sigma Cumul flags t u
   with e when precatchable_exception e -> ([],[])
@@ -613,11 +617,12 @@ let w_unify_meta_types env ?(flags=default_unify_flags) evd =
    types of metavars are unifiable with the types of their instances    *)
 
 let check_types env evd flags subst m n =
-  if isEvar (fst (whd_stack m)) or isEvar (fst (whd_stack n)) then
+  let sigma = evars_of evd in
+  if isEvar (fst (whd_stack sigma m)) or isEvar (fst (whd_stack sigma n)) then
     unify_0_with_initial_metas subst true env (evars_of evd) topconv 
       flags
-      (Retyping.get_type_of_with_meta env (evars_of evd) (metas_of evd) m)
-      (Retyping.get_type_of_with_meta env (evars_of evd) (metas_of evd) n)
+      (Retyping.get_type_of_with_meta env sigma (metas_of evd) m)
+      (Retyping.get_type_of_with_meta env sigma (metas_of evd) n)
   else
     subst
 
@@ -738,8 +743,8 @@ let secondOrderAbstraction env flags allow_K typ (p, oplist) evd =
   w_merge env false flags ([p,pred,(ConvUpToEta 0,TypeProcessed)],[]) evd'
 
 let w_unify2 env flags allow_K cv_pb ty1 ty2 evd =
-  let c1, oplist1 = whd_stack ty1 in
-  let c2, oplist2 = whd_stack ty2 in
+  let c1, oplist1 = whd_stack (evars_of evd) ty1 in
+  let c2, oplist2 = whd_stack (evars_of evd) ty2 in
   match kind_of_term c1, kind_of_term c2 with
     | Meta p1, _ ->
         (* Find the predicate *)
@@ -777,8 +782,8 @@ let w_unify2 env flags allow_K cv_pb ty1 ty2 evd =
    Meta(1) had meta-variables in it. *)
 let w_unify allow_K env cv_pb ?(flags=default_unify_flags) ty1 ty2 evd =
   let cv_pb = of_conv_pb cv_pb in
-  let hd1,l1 = whd_stack ty1 in
-  let hd2,l2 = whd_stack ty2 in
+  let hd1,l1 = whd_stack (evars_of evd) ty1 in
+  let hd2,l2 = whd_stack (evars_of evd) ty2 in
     match kind_of_term hd1, l1<>[], kind_of_term hd2, l2<>[] with
       (* Pattern case *)
       | (Meta _, true, Lambda _, _ | Lambda _, _, Meta _, true)
diff --git a/proofs/logic.ml b/proofs/logic.ml
index a04216cb..3e758eb6 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: logic.ml 11796 2009-01-18 13:41:39Z herbelin $ *)
+(* $Id: logic.ml 11897 2009-02-09 19:28:02Z barras $ *)
 
 open Pp
 open Util
@@ -336,7 +336,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 *)
   match kind_of_term trm with
     | Meta _ ->
-	let conclty = nf_betaiota conclty in
+	let conclty = nf_betaiota sigma conclty in
 	  if !check && occur_meta conclty then
 	    raise (RefinerError (MetaInType conclty));
 	  (mk_goal hyps conclty)::goalacc, conclty
@@ -390,7 +390,7 @@ and mk_hdgoals sigma goal goalacc trm =
   match kind_of_term trm with
     | Cast (c,_, ty) when isMeta c ->
 	check_typability env sigma ty;
-	(mk_goal hyps (nf_betaiota ty))::goalacc,ty
+	(mk_goal hyps (nf_betaiota sigma ty))::goalacc,ty
 
     | Cast (t,_, ty) ->
 	check_typability env sigma ty;
@@ -502,7 +502,7 @@ let prim_refiner r sigma goal =
 	       raise (RefinerError IntroNeedsProduct))
 	
     | Cut (b,replace,id,t) ->
-        let sg1 = mk_goal sign (nf_betaiota t) in
+        let sg1 = mk_goal sign (nf_betaiota sigma t) in
 	let sign,cl,sigma =
 	  if replace then
 	    let nexthyp = get_hyp_after id (named_context_of_val sign) in
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index a9a1f51d..7ce256bf 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: refiner.ml 11865 2009-01-28 17:34:30Z herbelin $ *)
+(* $Id: refiner.ml 11897 2009-02-09 19:28:02Z barras $ *)
 
 open Pp
 open Util
@@ -763,7 +763,7 @@ let extract_pftreestate pts =
       else
         str "Attempt to save a proof with existential variables still non-instantiated");
   let env = Global.env_of_context pts.tpf.goal.evar_hyps in
-  nf_betaiotaevar_preserving_vm_cast env pts.tpfsigma pfterm
+  nf_betaiota_preserving_vm_cast env pts.tpfsigma pfterm
   (* strong whd_betaiotaevar env pts.tpfsigma pfterm *)
   (***
   local_strong (Evarutil.whd_ise (ts_it pts.tpfsigma)) pfterm
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index bf194d47..6c4f7b5e 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tacmach.ml 11639 2008-11-27 17:48:32Z barras $ *)
+(* $Id: tacmach.ml 11897 2009-02-09 19:28:02Z barras $ *)
 
 open Pp
 open Util
@@ -99,7 +99,7 @@ let pf_whd_betadeltaiota_stack   = pf_reduce whd_betadeltaiota_stack
 let pf_hnf_constr                = pf_reduce hnf_constr
 let pf_red_product               = pf_reduce red_product
 let pf_nf                        = pf_reduce nf
-let pf_nf_betaiota               = pf_reduce (fun _ _ -> nf_betaiota)
+let pf_nf_betaiota               = pf_reduce (fun _ -> nf_betaiota)
 let pf_compute                   = pf_reduce compute
 let pf_unfoldn ubinds            = pf_reduce (unfoldn ubinds)
 let pf_type_of                   = pf_reduce type_of
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index e609fb77..6a425984 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -9,7 +9,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: class_tactics.ml4 11823 2009-01-21 15:32:37Z msozeau $ *)
+(* $Id: class_tactics.ml4 11897 2009-02-09 19:28:02Z barras $ *)
 
 open Pp
 open Util
@@ -650,14 +650,14 @@ let build_signature isevars env m (cstrs : 'a option list) (finalcstr : 'a Lazy.
       | Prod (na, ty, b), obj :: cstrs -> 
 	  if dependent (mkRel 1) b then
 	    let (b, arg, evars) = aux (Environ.push_rel (na, None, ty) env) b cstrs in
-	    let ty = Reductionops.nf_betaiota ty in
+	    let ty = Reductionops.nf_betaiota (Evd.evars_of !isevars) ty in
 	    let pred = mkLambda (na, ty, b) in
 	    let liftarg = mkLambda (na, ty, arg) in
 	    let arg' = mkApp (Lazy.force forall_relation, [| ty ; pred ; liftarg |]) in
 	      mkProd(na, ty, b), arg', (ty, None) :: evars
 	  else
 	    let (b', arg, evars) = aux env (subst1 mkProp b) cstrs in
-	    let ty = Reductionops.nf_betaiota ty in
+	    let ty = Reductionops.nf_betaiota(Evd.evars_of !isevars) ty in
 	    let relty = mk_relty ty obj in
 	    let newarg = mkApp (Lazy.force respectful, [| ty ; b' ; relty ; arg |]) in
 	      mkProd(na, ty, b), newarg, (ty, Some relty) :: evars
@@ -665,7 +665,7 @@ let build_signature isevars env m (cstrs : 'a option list) (finalcstr : 'a Lazy.
       | _, [] -> 
 	  (match finalcstr with
 	      None -> 
-		let t = Reductionops.nf_betaiota ty in
+		let t = Reductionops.nf_betaiota(Evd.evars_of !isevars) ty in
 		let rel = mk_relty t None in 
 		  t, rel, [t, Some rel]
 	    | Some codom -> let (t, rel) = Lazy.force codom in
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml
index 839a494a..2d0395a3 100644
--- a/tactics/decl_proof_instr.ml
+++ b/tactics/decl_proof_instr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: decl_proof_instr.ml 11671 2008-12-12 12:43:03Z herbelin $ *)
+(* $Id: decl_proof_instr.ml 11897 2009-02-09 19:28:02Z barras $ *)
 
 open Util
 open Pp
@@ -1093,7 +1093,7 @@ let thesis_for obj typ per_info env=
       ((Printer.pr_constr_env env obj) ++ spc () ++ 
 	 str "cannot give an induction hypothesis (wrong parameters).") in
   let hd2 = (applist ((lift (List.length rc) per_info.per_pred),args@[obj])) in
-    compose_prod rc (whd_beta hd2)
+    compose_prod rc (whd_beta Evd.empty hd2)
 
 let rec build_product_dep pat_info per_info args body gls =
   match args with 
@@ -1225,7 +1225,7 @@ let hrec_for fix_id per_info gls obj_id =
     try List.for_all2 eq_constr params per_info.per_params with 
         Invalid_argument _ -> false end;
   let hd2 = applist (mkVar fix_id,args@[obj]) in 
-    compose_lam rc (whd_beta hd2)
+    compose_lam rc (whd_beta gls.sigma hd2)
 
 let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
   match tree, objs  with
diff --git a/tactics/equality.ml b/tactics/equality.ml
index ba18430a..baebee07 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: equality.ml 11800 2009-01-18 18:34:15Z msozeau $ *)
+(* $Id: equality.ml 11897 2009-02-09 19:28:02Z barras $ *)
 
 open Pp
 open Util
@@ -120,7 +120,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs ((c,l) : open_constr with_
     let sigma, c' = c in
     let sigma = Evd.merge sigma (project gl) in
     let ctype = get_type_of env sigma c' in 
-    let rels, t = decompose_prod (whd_betaiotazeta ctype) in
+    let rels, t = decompose_prod (whd_betaiotazeta sigma ctype) in
       match match_with_equality_type t with
       | Some (hdcncl,args) -> (* Fast path: direct leibniz rewrite *)
 	  let lft2rgt = adjust_rewriting_direction args lft2rgt in
@@ -737,7 +737,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
       else
 	error "Cannot solve an unification problem."
     else
-      let (a,p_i_minus_1) = match whd_beta_stack p_i with
+      let (a,p_i_minus_1) = match whd_beta_stack (evars_of !evdref) p_i with
 	| (_sigS,[a;p]) -> (a,p)
  	| _ -> anomaly "sig_clausal_form: should be a sigma type" in
       let ev = Evarutil.e_new_evar evdref env a in
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 5acc5197..e798f59a 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: leminv.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: leminv.ml 11897 2009-02-09 19:28:02Z barras $ *)
 
 open Pp
 open Util
@@ -237,7 +237,8 @@ let inversion_scheme env sigma t sort dep_option inv_op =
       meta_types 
   in
   let invProof = 
-    it_mkNamedLambda_or_LetIn (local_strong (whd_meta mvb) pfterm) ownSign 
+    it_mkNamedLambda_or_LetIn
+      (local_strong (fun _ -> whd_meta mvb) Evd.empty pfterm) ownSign 
   in
   invProof
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 5af5c0d5..2c567034 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tactics.ml 11745 2009-01-04 18:43:08Z herbelin $ *)
+(* $Id: tactics.ml 11897 2009-02-09 19:28:02Z barras $ *)
 
 open Pp
 open Util
@@ -759,7 +759,7 @@ let general_apply with_delta with_destruct with_evars (c,lbind) gl0 =
   let concl_nprod = nb_prod (pf_concl gl0) in
   let evm, c = c in
   let rec try_main_apply c gl =
-    let thm_ty0 = nf_betaiota (pf_type_of gl c) in
+    let thm_ty0 = nf_betaiota (project gl) (pf_type_of gl c) in
     let try_apply thm_ty nprod =
       let n = nb_prod thm_ty - nprod in
 	if n<0 then error "Applied theorem has not enough premisses.";
@@ -850,7 +850,7 @@ let progress_with_clause flags innerclause clause =
   with Failure _ -> error "Unable to unify."
 
 let apply_in_once_main flags innerclause (d,lbind) gl =
-  let thm = nf_betaiota (pf_type_of gl d) in
+  let thm = nf_betaiota gl.sigma (pf_type_of gl d) in
   let rec aux clause =
     try progress_with_clause flags innerclause clause
     with err ->
@@ -985,7 +985,8 @@ let specialize mopt (c,lbind) g =
     else 
       let clause = make_clenv_binding g (c,pf_type_of g c) lbind in
       let clause = clenv_unify_meta_types clause in
-      let (thd,tstack) = whd_stack (clenv_value clause) in
+      let (thd,tstack) =
+        whd_stack (evars_of clause.evd) (clenv_value clause) in
       let nargs = List.length tstack in
       let tstack = match mopt with 
 	| Some m -> 
diff --git a/test-suite/complexity/unification.v b/test-suite/complexity/unification.v
new file mode 100644
index 00000000..0e1ec00d
--- /dev/null
+++ b/test-suite/complexity/unification.v
@@ -0,0 +1,51 @@
+(* Test parsing/interpretation/pretyping on a large example *)
+(* Expected time < 0.10s *)
+
+(* Complexity of unification used to be exponential in the number of nested
+   constants, as pointed out by Georges Gonthier and Nicolas Tabareau (a.o.)
+
+   The problem is that unification of id^n+1(0) and id^n+1(1) proceeds as:
+   - try not unfold the outermost id by trying to unify its arguments:
+     1st rec. call on id^n(0) id^n(1), which fails
+   - Coq then tries to unfold id^n+1(k) which produces id^n(k)
+   - 2nd rec. call on id^n(0) id^n(1), which also fails
+   Complexity is thus at least exponential.
+
+   This is fixed (in the ground case), by the fact that when we try to
+   unify two ground terms (ie. without unsolved evars), we call kernel
+   conversion and if this fails, then the terms are not unifiable.
+   Hopefully, kernel conversion is not exponential on cases like the one
+   below thanks to sharing (as long as unfolding the fonction does not
+   use its argument under a binder).
+
+   There are probably still many cases where unification goes astray.
+ *)
+
+
+Definition id (n:nat) := n.
+Goal
+  (id (id (id (id
+  (id (id (id (id
+  (id (id (id (id
+  (id (id (id (id
+  (id (id (id (id
+   0
+   ))))
+   ))))
+   ))))
+   ))))
+   ))))
+   =
+  (id (id (id (id
+  (id (id (id (id
+  (id (id (id (id
+  (id (id (id (id
+  (id (id (id (id
+   1
+   ))))
+   ))))
+   ))))
+   ))))
+   ))))
+.
+Time try refine (refl_equal _).
diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index 4d655eac..6da1c6ec 100644
--- a/theories/Numbers/Cyclic/Int31/Cyclic31.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Cyclic31.v 11034 2008-06-02 08:15:34Z thery $ i*)
+(*i $Id: Cyclic31.v 11907 2009-02-10 23:54:28Z letouzey $ i*)
 
 (** * Int31 numbers defines indeed a cyclic structure : Z/(2^31)Z *)
 
@@ -1637,7 +1637,12 @@ Section Int31_Spec.
  apply Zplus_eq_compat.
  ring.
  assert ((2*[|y|]) mod wB = 2*[|y|] - wB).
-  admit.
+  clear - H. symmetry. apply Zmod_unique with 1; [ | ring ].
+  generalize (phi_lowerbound  _ H) (phi_bounded y).
+  set (wB' := 2^Z_of_nat (pred size)).
+  replace wB with (2*wB'); [ omega | ].
+  unfold wB'. rewrite <- Zpower_Zsucc, <- inj_S by (auto with zarith).
+  f_equal.
  rewrite H1.
  replace wB with (2^(Z_of_nat n)*2^(31-Z_of_nat n)) by  
   (rewrite <- Zpower_exp; auto with zarith; f_equal; unfold size; ring).
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 19bdeccd..c07b86a6 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: RIneq.v 10762 2008-04-06 16:57:31Z herbelin $ i*)
+(*i $Id: RIneq.v 11887 2009-02-06 19:57:33Z herbelin $ i*)
 
 (*********************************************************)
 (** * Basic lemmas for the classical real numbers        *)
@@ -1200,7 +1200,7 @@ Hint Resolve Rmult_le_compat: real.
 
 Lemma Rmult_ge_compat :
   forall r1 r2 r3 r4,
-    0 <= r1 -> 0 <= r3 -> r1 <= r2 -> r3 <= r4 -> r1 * r3 <= r2 * r4.
+    r2 >= 0 -> r4 >= 0 -> r1 >= r2 -> r3 >= r4 -> r1 * r3 >= r2 * r4.
 Proof. auto with real rorders. Qed.
 
 Lemma Rmult_gt_0_lt_compat :
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index 3fbf71dd..98457261 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coq_makefile.ml4 11771 2009-01-09 18:00:56Z notin $ *)
+(* $Id: coq_makefile.ml4 11883 2009-02-06 09:54:52Z herbelin $ *)
 
 (* créer un Makefile pour un développement Coq automatiquement *)
 
@@ -248,6 +248,7 @@ let implicit () =
     print "%.cmxs: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $(PP) $<\n\n";
     print "%.cmo: %.ml4\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n";
     print "%.cmx: %.ml4\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n";
+    print "%.cmxs: %.ml4\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $(PP) -impl $<\n\n";
     print "%.ml.d: %.ml\n";
     print "\t$(CAMLBIN)ocamldep -slash $(COQSRCLIBS) $(PP) \"$<\" > \"$@\"\n\n"
   and v_rule () =