Imported Upstream version 8.4~betaupstream/8.4_beta

31 files changed, 959 insertions, 1372 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 40119a7e..bb42b949 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -1,18 +1,15 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: library.ml 9679 2007-02-24 15:22:07Z herbelin $ *)
-
 open Pp
 open Util
 open Names
 
-let pr_id id = str (string_of_id id)
 let pr_dirpath dp = str (string_of_dirpath dp)
 let default_root_prefix = make_dirpath []
 let split_dirpath d =
@@ -42,7 +39,7 @@ type compilation_unit_name = dir_path
 
 type library_disk = {
   md_name : compilation_unit_name;
-  md_compiled : Safe_typing.compiled_library;
+  md_compiled : Safe_typing.LightenLibrary.lightened_compiled_library;
   md_objects : library_objects;
   md_deps : (compilation_unit_name * Digest.t) list;
   md_imports : compilation_unit_name list }
@@ -155,12 +152,6 @@ let find_logical_path phys_dir =
   | _,[] -> default_root_prefix
   | _,l -> anomaly ("Two logical paths are associated to "^phys_dir)
 
-let is_in_load_paths phys_dir =
-  let dir = canonical_path_name phys_dir in
-  let lp = get_load_paths () in
-  let check_p = fun p -> (String.compare dir p) == 0 in
-    List.exists check_p lp
-
 let remove_load_path dir =
   load_paths := list_filter2 (fun p d -> p <> dir) !load_paths
 
@@ -191,13 +182,9 @@ let add_load_path (phys_path,coq_path) =
 	  load_paths := (phys_path :: fst !load_paths, coq_path :: snd !load_paths)
       | _ -> anomaly ("Two logical paths are associated to "^phys_path)
 
-let physical_paths (dp,lp) = dp
-
 let load_paths_of_dir_path dir =
   fst (list_filter2 (fun p d -> d = dir) !load_paths)
 
-let get_full_load_paths () = List.combine (fst !load_paths) (snd !load_paths)
-
 (************************************************************************)
 (*s Locate absolute or partially qualified library names in the path *)
 
@@ -269,8 +256,8 @@ let try_locate_qualified_library qid =
 
 (*s Loading from disk to cache (preparation phase) *)
 
-let (raw_extern_library, raw_intern_library) =
-  System.raw_extern_intern Coq_config.vo_magic_number ".vo"
+let raw_intern_library =
+  snd (System.raw_extern_intern Coq_config.vo_magic_number ".vo")
 
 let with_magic_number_check f a =
   try f a
@@ -283,10 +270,10 @@ let with_magic_number_check f a =
 (************************************************************************)
 (* Internalise libraries *)
 
-let mk_library md f digest = {
+let mk_library md f table digest = {
   library_name = md.md_name;
   library_filename = f;
-  library_compiled = md.md_compiled;
+  library_compiled = Safe_typing.LightenLibrary.load table md.md_compiled;
   library_deps = md.md_deps;
   library_digest = digest }
 
@@ -300,20 +287,21 @@ let depgraph = ref LibraryMap.empty
 
 let intern_from_file (dir, f) =
   Flags.if_verbose msg (str"[intern "++str f++str" ...");
-  let (md,digest) =
+  let (md,table,digest) =
     try
       let ch = with_magic_number_check raw_intern_library f in
       let (md:library_disk) = System.marshal_in ch in
       let digest = System.marshal_in ch in
+      let table = (System.marshal_in ch : Safe_typing.LightenLibrary.table) in
       close_in ch;
       if dir <> md.md_name then
         errorlabstrm "load_physical_library"
           (name_clash_message dir md.md_name f);
       Flags.if_verbose msgnl(str" done]");
-      md,digest
+      md,table,digest
     with e -> Flags.if_verbose msgnl(str" failed!]"); raise e in
   depgraph := LibraryMap.add md.md_name md.md_deps !depgraph;
-  mk_library md f digest
+  mk_library md f table digest
 
 let get_deps (dir, f) =
   try LibraryMap.find dir !depgraph
diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index 88f2374b..5f28269e 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -37,7 +37,7 @@ let cst_filter f csts =
     (fun c ce acc -> if f c ce then c::acc else acc)
     csts []
 
-let is_ax _ cb = cb.const_body = None
+let is_ax _ cb = not (constant_has_body cb)
 
 let pr_ax csts =
   let axs = cst_filter is_ax csts in
diff --git a/checker/check_stat.mli b/checker/check_stat.mli
index d39eb454..353edda6 100644
--- a/checker/check_stat.mli
+++ b/checker/check_stat.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/checker/checker.ml b/checker/checker.ml
index 76f81264..34ba7b01 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -1,13 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqtop.ml 10153 2007-09-28 18:00:45Z glondu $ *)
-
+open Compat
 open Pp
 open Util
 open System
@@ -32,11 +31,11 @@ let parse_dir s =
     decoupe_dirs [] 0
 let dirpath_of_string s =
   match parse_dir s with
-      [] -> invalid_arg "dirpath_of_string"
+      [] -> Check.default_root_prefix
     | dir -> make_dirpath (List.map id_of_string dir)
 let path_of_string s =
   match parse_dir s with
-      [] -> invalid_arg "dirpath_of_string"
+      [] -> invalid_arg "path_of_string"
     | l::dir -> {dirpath=dir; basename=l}
 
 let (/) = Filename.concat
@@ -73,17 +72,17 @@ let convert_string d =
     flush_all ();
     failwith "caught"
 
-let add_rec_path ~unix_path:dir ~coq_root:coq_dirpath =
-  if exists_dir dir then
-    let dirs = all_subdirs dir in
-    let prefix = repr_dirpath coq_dirpath in
+let add_rec_path ~unix_path ~coq_root =
+  if exists_dir unix_path then
+    let dirs = all_subdirs ~unix_path in
+    let prefix = repr_dirpath coq_root in
     let convert_dirs (lp,cp) =
       (lp,make_dirpath (List.map convert_string (List.rev cp)@prefix)) in
     let dirs = map_succeed convert_dirs dirs in
     List.iter Check.add_load_path dirs;
-    Check.add_load_path (dir,coq_dirpath)
+    Check.add_load_path (unix_path, coq_root)
   else
-    msg_warning (str ("Cannot open " ^ dir))
+    msg_warning (str ("Cannot open " ^ unix_path))
 
 (* By the option -include -I or -R of the command line *)
 let includes = ref []
@@ -92,9 +91,6 @@ let push_rec_include (s, alias) = includes := (s,alias,true) :: !includes
 
 let set_default_include d =
   push_include (d, Check.default_root_prefix)
-let set_default_rec_include d =
-  let p = Check.default_root_prefix in
-  push_rec_include (d, p)
 let set_include d p =
   let p = dirpath_of_string p in
   push_include (d,p)
@@ -106,24 +102,27 @@ let set_rec_include d p =
 let init_load_path () =
   let coqlib = Envars.coqlib () in
   let user_contrib = coqlib/"user-contrib" in
+  let xdg_dirs = Envars.xdg_dirs in
+  let coqpath = Envars.coqpath in
   let plugins = coqlib/"plugins" in
-  (* first user-contrib *)
-  if Sys.file_exists user_contrib then
-    add_rec_path user_contrib Check.default_root_prefix;
+  (* NOTE: These directories are searched from last to first *)
+  (* first standard library *)
+  add_rec_path ~unix_path:(coqlib/"theories") ~coq_root:(Names.make_dirpath[coq_root]);
   (* then plugins *)
-  add_rec_path plugins (Names.make_dirpath [coq_root]);
-  (* then standard library *)
-(*  List.iter
-    (fun (s,alias) ->
-      add_rec_path (coqlib/s) ([alias; coq_root]))
-    theories_dirs_map;*)
-  add_rec_path (coqlib/"theories") (Names.make_dirpath[coq_root]);
+  add_rec_path ~unix_path:plugins ~coq_root:(Names.make_dirpath [coq_root]);
+  (* then user-contrib *)
+  if Sys.file_exists user_contrib then
+    add_rec_path ~unix_path:user_contrib ~coq_root:Check.default_root_prefix;
+  (* then directories in XDG_DATA_DIRS and XDG_DATA_HOME *)
+  List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix) xdg_dirs;
+  (* then directories in COQPATH *)
+  List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix) coqpath;
   (* then current directory *)
-  add_path "." Check.default_root_prefix;
+  add_path ~unix_path:"." ~coq_root:Check.default_root_prefix;
   (* additional loadpath, given with -I -include -R options *)
   List.iter
-    (fun (s,alias,reci) ->
-      if reci then add_rec_path s alias else add_path s alias)
+    (fun (unix_path, coq_root, reci) ->
+      if reci then add_rec_path ~unix_path ~coq_root else add_path ~unix_path ~coq_root)
     (List.rev !includes);
   includes := []
 
@@ -168,43 +167,41 @@ let version () =
 
 let print_usage_channel co command =
   output_string co command;
-  output_string co "Coq options are:\n";
+  output_string co "coqchk options are:\n";
   output_string co
-"  -I dir -as coqdir      map physical dir to logical coqdir
-  -I dir                 map directory dir to the empty logical path
-  -include dir           (idem)
-  -R dir -as coqdir      recursively map physical dir to logical coqdir
-  -R dir coqdir          (idem)
-
-  -admit module          load module and dependencies without checking
-  -norec module          check module but admit dependencies without checking
-
-  -where                 print Coq's standard library location and exit
-  -v                     print Coq version and exit
-  -boot                  boot mode
-  -o, --output-context   print the list of assumptions
-  -m, --memoty           print the maximum heap size
-  -silent                disable trace of constants being checked
-
-  -impredicative-set     set sort Set impredicative
-
-  -h, --help             print this list of options
-"
+"  -I dir -as coqdir      map physical dir to logical coqdir\
+\n  -I dir                 map directory dir to the empty logical path\
+\n  -include dir           (idem)\
+\n  -R dir -as coqdir      recursively map physical dir to logical coqdir\
+\n  -R dir coqdir          (idem)\
+\n\
+\n  -admit module          load module and dependencies without checking\
+\n  -norec module          check module but admit dependencies without checking\
+\n\
+\n  -where                 print coqchk's standard library location and exit\
+\n  -v                     print coqchk version and exit\
+\n  -boot                  boot mode\
+\n  -o, --output-context   print the list of assumptions\
+\n  -m, --memory           print the maximum heap size\
+\n  -silent                disable trace of constants being checked\
+\n\
+\n  -impredicative-set     set sort Set impredicative\
+\n\
+\n  -h, --help             print this list of options\
+\n"
 
 (* print the usage on standard error *)
 
 let print_usage = print_usage_channel stderr
 
 let print_usage_coqtop () =
-  print_usage "Usage: coqchk <options>\n\n"
+  print_usage "Usage: coqchk <options> modules\n\n"
 
 let usage () =
   print_usage_coqtop ();
   flush stderr;
   exit 1
 
-let warning s = msg_warning (str s)
-
 open Type_errors
 
 let anomaly_string () = str "Anomaly: "
@@ -239,14 +236,9 @@ let rec explain_exn = function
   | Anomaly (s,pps) ->
       hov 1 (anomaly_string () ++ where s ++ pps ++ report ())
   | Match_failure(filename,pos1,pos2) ->
-      hov 1 (anomaly_string () ++ str "Match failure in file " ++ str (guill filename) ++
-      if Sys.ocaml_version = "3.06" then
-		   (str " from character " ++ int pos1 ++
-                    str " to " ++ int pos2)
-		 else
-		   (str " at line " ++ int pos1 ++
-		    str " character " ++ int pos2)
-	           ++ report ())
+      hov 1 (anomaly_string () ++ str "Match failure in file " ++
+	     str (guill filename) ++ str " at line " ++ int pos1 ++
+	     str " character " ++ int pos2 ++ report ())
   | Not_found ->
       hov 0 (anomaly_string () ++ str "uncaught exception Not_found" ++ report ())
   | Failure s ->
@@ -274,22 +266,17 @@ let rec explain_exn = function
 (*      let ctx = Check.get_env() in
       hov 0
         (str "Error:" ++ spc () ++ Himsg.explain_inductive_error ctx e)*)
-  | Stdpp.Exc_located (loc,exc) ->
+  | Loc.Exc_located (loc,exc) ->
       hov 0 ((if loc = dummy_loc then (mt ())
                else (str"At location " ++ print_loc loc ++ str":" ++ fnl ()))
                ++ explain_exn exc)
   | Assert_failure (s,b,e) ->
       hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++
-	       (if s <> "" then
-		 if Sys.ocaml_version = "3.06" then
-		   (str ("(file \"" ^ s ^ "\", characters ") ++
-		    int b ++ str "-" ++ int e ++ str ")")
-		 else
-		   (str ("(file \"" ^ s ^ "\", line ") ++ int b ++
-		    str ", characters " ++ int e ++ str "-" ++
-		    int (e+6) ++ str ")")
-	       else
-		 (mt ())) ++
+	       (if s = "" then mt ()
+		else
+		  (str ("(file \"" ^ s ^ "\", line ") ++ int b ++
+		   str ", characters " ++ int e ++ str "-" ++
+		   int (e+6) ++ str ")")) ++
 	       report ())
   | reraise ->
       hov 0 (anomaly_string () ++ str "Uncaught exception " ++
@@ -298,8 +285,15 @@ let rec explain_exn = function
 let parse_args argv =
   let rec parse = function
     | [] -> ()
-   | "-impredicative-set" :: rem ->
-       set_engagement Declarations.ImpredicativeSet; parse rem
+    | "-impredicative-set" :: rem ->
+      set_engagement Declarations.ImpredicativeSet; parse rem
+
+    | "-coqlib" :: s :: rem ->
+      if not (exists_dir s) then 
+	(msgnl (str ("Directory '"^s^"' does not exist")); exit 1);
+      Flags.coqlib := s;
+      Flags.coqlib_spec := true;
+      parse rem
 
     | ("-I"|"-include") :: d :: "-as" :: p :: rem -> set_include d p; parse rem
     | ("-I"|"-include") :: d :: "-as" :: [] -> usage ()
diff --git a/checker/closure.ml b/checker/closure.ml
index da25b3b3..033e2bd7 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: closure.ml 9983 2007-07-12 17:15:22Z barras $ *)
-
 open Util
 open Pp
 open Term
@@ -54,6 +52,9 @@ type transparent_state = Idpred.t * Cpred.t
 let all_opaque = (Idpred.empty, Cpred.empty)
 let all_transparent = (Idpred.full, Cpred.full)
 
+let is_transparent_variable (ids, _) id = Idpred.mem id ids
+let is_transparent_constant (_, csts) cst = Cpred.mem cst csts
+
 module type RedFlagsSig = sig
   type reds
   type red_kind
@@ -65,11 +66,8 @@ module type RedFlagsSig = sig
   val fVAR : identifier -> red_kind
   val no_red : reds
   val red_add : reds -> red_kind -> reds
-  val red_sub : reds -> red_kind -> reds
-  val red_add_transparent : reds -> transparent_state -> reds
   val mkflags : red_kind list -> reds
   val red_set : reds -> red_kind -> bool
-  val red_get_const : reds -> bool * evaluable_global_reference list
 end
 
 module RedFlags = (struct
@@ -114,21 +112,6 @@ module RedFlags = (struct
 	let (l1,l2) = red.r_const in
 	{ red with r_const = Idpred.add id l1, l2 }
 
-  let red_sub red = function
-    | BETA -> { red with r_beta = false }
-    | DELTA -> { red with r_delta = false }
-    | CONST kn ->
- 	let (l1,l2) = red.r_const in
-	{ red with r_const = l1, Cpred.remove kn l2 }
-    | IOTA -> { red with r_iota = false }
-    | ZETA -> { red with r_zeta = false }
-    | VAR id ->
-	let (l1,l2) = red.r_const in
-	{ red with r_const = Idpred.remove id l1, l2 }
-
-  let red_add_transparent red tr =
-    { red with r_const = tr }
-
   let mkflags = List.fold_left red_add no_red
 
   let red_set red = function
@@ -146,160 +129,14 @@ module RedFlags = (struct
     | DELTA -> (* Used for Rel/Var defined in context *)
 	incr_cnt red.r_delta delta
 
-  let red_get_const red =
-    let p1,p2 = red.r_const in
-    let (b1,l1) = Idpred.elements p1 in
-    let (b2,l2) = Cpred.elements p2 in
-    if b1=b2 then
-      let l1' = List.map (fun x -> EvalVarRef x) l1 in
-      let l2' = List.map (fun x -> EvalConstRef x) l2 in
-      (b1, l1' @ l2')
-    else error "unrepresentable pair of predicate"
-
 end : RedFlagsSig)
 
 open RedFlags
 
 let betadeltaiota = mkflags [fBETA;fDELTA;fZETA;fIOTA]
 let betadeltaiotanolet = mkflags [fBETA;fDELTA;fIOTA]
-let betaiota = mkflags [fBETA;fIOTA]
-let beta = mkflags [fBETA]
 let betaiotazeta = mkflags [fBETA;fIOTA;fZETA]
-let unfold_red kn =
-  let flag = match kn with
-    | EvalVarRef id -> fVAR id
-    | EvalConstRef kn -> fCONST kn
-  in (* Remove fZETA for finer behaviour ? *)
-  mkflags [fBETA;flag;fIOTA;fZETA]
-
-(************************* Obsolète
-(* [r_const=(true,cl)] means all constants but those in [cl] *)
-(* [r_const=(false,cl)] means only those in [cl] *)
-type reds = {
-  r_beta : bool;
-  r_const : bool * constant_path list * identifier list;
-  r_zeta : bool;
-  r_evar : bool;
-  r_iota : bool }
-
-let betadeltaiota_red = {
-  r_beta = true;
-  r_const = true,[],[];
-  r_zeta = true;
-  r_evar = true;
-  r_iota = true }
-
-let betaiota_red = {
-  r_beta = true;
-  r_const = false,[],[];
-  r_zeta = false;
-  r_evar = false;
-  r_iota = true }
-
-let beta_red = {
-  r_beta = true;
-  r_const = false,[],[];
-  r_zeta = false;
-  r_evar = false;
-  r_iota = false }
-
-let no_red = {
-  r_beta = false;
-  r_const = false,[],[];
-  r_zeta = false;
-  r_evar = false;
-  r_iota = false }
-
-let betaiotazeta_red = {
-  r_beta = true;
-  r_const = false,[],[];
-  r_zeta = true;
-  r_evar = false;
-  r_iota = true }
-
-let unfold_red kn =
-  let c = match kn with
-    | EvalVarRef id -> false,[],[id]
-    | EvalConstRef kn -> false,[kn],[]
-  in {
-  r_beta = true;
-  r_const = c;
-  r_zeta = true;   (* false for finer behaviour ? *)
-  r_evar = false;
-  r_iota = true }
-
-(* Sets of reduction kinds.
-   Main rule: delta implies all consts (both global (= by
-   kernel_name) and local (= by Rel or Var)), all evars, and zeta (= letin's).
-   Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of
-   a LetIn expression is Letin reduction *)
-
-type red_kind =
-    BETA | DELTA | ZETA | IOTA
-  | CONST of constant_path list | CONSTBUT of constant_path list
-  | VAR of identifier | VARBUT of identifier
-
-let rec red_add red = function
-  | BETA -> { red with r_beta = true }
-  | DELTA ->
-      (match red.r_const with
-	| _,_::_,[] | _,[],_::_ -> error "Conflict in the reduction flags"
-	| _ -> { red with r_const = true,[],[]; r_zeta = true; r_evar = true })
-  | CONST cl ->
-      (match red.r_const with
-	| true,_,_ -> error "Conflict in the reduction flags"
-	| _,l1,l2 -> { red with r_const = false, list_union cl l1, l2 })
-  | CONSTBUT cl ->
-      (match red.r_const with
-	| false,_::_,_ | false,_,_::_ ->
-			   error "Conflict in the reduction flags"
-	| _,l1,l2 ->
-	    { red with r_const = true, list_union cl l1, l2;
-		r_zeta = true; r_evar = true })
-  | IOTA -> { red with r_iota = true }
-  | ZETA -> { red with r_zeta = true }
-  | VAR id ->
-      (match red.r_const with
-	| true,_,_ -> error "Conflict in the reduction flags"
-	| _,l1,l2 -> { red with r_const = false, l1, list_union [id] l2 })
-  | VARBUT cl ->
-      (match red.r_const with
-	| false,_::_,_ | false,_,_::_ ->
-			   error "Conflict in the reduction flags"
-	| _,l1,l2 ->
-	    { red with r_const = true, l1, list_union [cl] l2;
-		r_zeta = true; r_evar = true })
-
-let red_delta_set red =
-  let b,_,_ = red.r_const in b
-
-let red_local_const = red_delta_set
-
-(* to know if a redex is allowed, only a subset of red_kind is used ... *)
-let red_set red = function
-  | BETA -> incr_cnt red.r_beta beta
-  | CONST [kn] ->
-      let (b,l,_) = red.r_const in
-      let c = List.mem kn l in
-      incr_cnt ((b & not c) or (c & not b)) delta
-  | VAR id -> (* En attendant d'avoir des kn pour les Var *)
-     let (b,_,l) = red.r_const in
-      let c = List.mem id l in
-      incr_cnt ((b & not c) or (c & not b)) delta
-  | ZETA -> incr_cnt red.r_zeta zeta
-  | EVAR -> incr_cnt red.r_zeta evar
-  | IOTA -> incr_cnt red.r_iota iota
-  | DELTA -> red_delta_set red (*Used for Rel/Var defined in context*)
-  (* Not for internal use *)
-  | CONST _ | CONSTBUT _ | VAR _ | VARBUT _ -> failwith "not implemented"
-
-(* Gives the constant list *)
-let red_get_const red =
-  let b,l1,l2 = red.r_const in
-  let l1' = List.map (fun x -> EvalConstRef x) l1 in
-  let l2' = List.map (fun x -> EvalVarRef x) l2 in
-  b, l1' @ l2'
-fin obsolète **************)
+
 (* specification of the reduction function *)
 
 
@@ -336,8 +173,6 @@ type 'a infos = {
   i_vars : (identifier * constr) list;
   i_tab : (table_key, 'a) Hashtbl.t }
 
-let info_flags info = info.i_flags
-
 let ref_value_cache info ref =
   try
     Some (Hashtbl.find info.i_tab ref)
@@ -447,9 +282,6 @@ and fterm =
 
 let fterm_of v = v.term
 let set_norm v = v.norm <- Norm
-let is_val v = v.norm = Norm
-
-let mk_atom c = {norm=Norm;term=FAtom c}
 
 (* Could issue a warning if no is still Red, pointing out that we loose
    sharing. *)
@@ -472,7 +304,6 @@ type stack_member =
 
 and stack = stack_member list
 
-let empty_stack = []
 let append_stack v s =
   if Array.length v = 0 then s else
   match s with
@@ -486,52 +317,6 @@ let zshift n s =
     | (_,Zshift(k)::s) -> Zshift(n+k)::s
     | _ -> Zshift(n)::s
 
-let rec stack_args_size = function
-  | Zapp v :: s -> Array.length v + stack_args_size s
-  | Zshift(_)::s -> stack_args_size s
-  | Zupdate(_)::s -> stack_args_size s
-  | _ -> 0
-
-(* When used as an argument stack (only Zapp can appear) *)
-let rec decomp_stack = function
-  | Zapp v :: s ->
-      (match Array.length v with
-          0 -> decomp_stack s
-        | 1 -> Some (v.(0), s)
-        | _ ->
-            Some (v.(0), (Zapp (Array.sub v 1 (Array.length v - 1)) :: s)))
-  | _ -> None
-let array_of_stack s =
-  let rec stackrec = function
-  | [] -> []
-  | Zapp args :: s -> args :: (stackrec s)
-  | _ -> assert false
-  in Array.concat (stackrec s)
-let rec stack_assign s p c = match s with
-  | Zapp args :: s ->
-      let q = Array.length args in
-      if p >= q then
-	Zapp args :: stack_assign s (p-q) c
-      else
-        (let nargs = Array.copy args in
-         nargs.(p) <- c;
-         Zapp nargs :: s)
-  | _ -> s
-let rec stack_tail p s =
-  if p = 0 then s else
-    match s with
-      | Zapp args :: s ->
-	  let q = Array.length args in
-	  if p >= q then stack_tail (p-q) s
-	  else Zapp (Array.sub args p (q-p)) :: s
-      | _ -> failwith "stack_tail"
-let rec stack_nth s p = match s with
-  | Zapp args :: s ->
-      let q = Array.length args in
-      if p >= q then stack_nth s (p-q)
-      else args.(p)
-  | _ -> raise Not_found
-
 (* Lifting. Preserves sharing (useful only for cell with norm=Red).
    lft_fconstr always create a new cell, while lift_fconstr avoids it
    when the lift is 0. *)
@@ -643,7 +428,7 @@ let optimise_closure env c =
     let (c',(_,s)) = compact_constr (0,[]) c 1 in
     let env' =
       Array.map (fun i -> clos_rel env i) (Array.of_list s) in
-    (subs_cons (env', ESID 0),c')
+    (subs_cons (env', subs_id 0),c')
 
 let mk_lambda env t =
   let (env,t) = optimise_closure env t in
@@ -774,7 +559,7 @@ let term_of_fconstr =
       | FFix(fx,e) when is_subs_id e & is_lift_id lfts -> Fix fx
       | FCoFix(cfx,e) when is_subs_id e & is_lift_id lfts -> CoFix cfx
       | _ -> to_constr term_of_fconstr_lift lfts v in
-  term_of_fconstr_lift ELID
+  term_of_fconstr_lift el_id
 
 
 
@@ -809,16 +594,6 @@ let fapp_stack (m,stk) = zip m stk
    (strip_update_shift, through get_arg). *)
 
 (* optimised for the case where there are no shifts... *)
-let strip_update_shift head stk =
-  assert (head.norm <> Red);
-  let rec strip_rec h depth = function
-    | Zshift(k)::s -> strip_rec (lift_fconstr k h) (depth+k) s
-    | Zupdate(m)::s ->
-        strip_rec (update m (h.norm,h.term)) depth s
-    | stk -> (depth,stk) in
-  strip_rec head 0 stk
-
-(* optimised for the case where there are no shifts... *)
 let strip_update_shift_app head stk =
   assert (head.norm <> Red);
   let rec strip_rec rstk h depth = function
@@ -835,15 +610,15 @@ let strip_update_shift_app head stk =
 
 let get_nth_arg head n stk =
   assert (head.norm <> Red);
-  let rec strip_rec rstk h depth n = function
+  let rec strip_rec rstk h n = function
     | Zshift(k) as e :: s ->
-        strip_rec (e::rstk) (lift_fconstr k h) (depth+k) n s
+        strip_rec (e::rstk) (lift_fconstr k h) n s
     | Zapp args::s' ->
         let q = Array.length args in
         if n >= q
         then
           strip_rec (Zapp args::rstk)
-            {norm=h.norm;term=FApp(h,args)} depth (n-q) s'
+            {norm=h.norm;term=FApp(h,args)} (n-q) s'
         else
           let bef = Array.sub args 0 n in
           let aft = Array.sub args (n+1) (q-n-1) in
@@ -851,9 +626,9 @@ let get_nth_arg head n stk =
             List.rev (if n = 0 then rstk else (Zapp bef :: rstk)) in
           (Some (stk', args.(n)), append_stack aft s')
     | Zupdate(m)::s ->
-        strip_rec rstk (update m (h.norm,h.term)) depth n s
+        strip_rec rstk (update m (h.norm,h.term)) n s
     | s -> (None, List.rev rstk @ s) in
-  strip_rec [] head 0 n stk
+  strip_rec [] head n stk
 
 (* Beta reduction: look for an applied argument in the stack.
    Since the encountered update marks are removed, h must be a whnf *)
@@ -876,6 +651,12 @@ let rec get_args n tys f e stk =
           get_args (n-na) etys f (subs_cons(l,e)) s
     | _ -> (Inr {norm=Cstr;term=FLambda(n,tys,f,e)}, stk)
 
+(* Eta expansion: add a reference to implicit surrounding lambda at end of stack *)
+let rec eta_expand_stack = function
+  | (Zapp _ | Zfix _ | Zcase _ | Zshift _ | Zupdate _ as e) :: s ->
+      e :: eta_expand_stack s
+  | [] ->
+      [Zshift 1; Zapp [|{norm=Norm; term= FRel 1}|]]
 
 (* Iota reduction: extract the arguments to be passed to the Case
    branches *)
@@ -1025,7 +806,7 @@ let kh info v stk = fapp_stack(kni info v stk)
 let whd_val info v =
   with_stats (lazy (term_of_fconstr (kh info v [])))
 
-let inject = mk_clos (ESID 0)
+let inject = mk_clos (subs_id 0)
 
 let whd_stack infos m stk =
   let k = kni infos m stk in
diff --git a/checker/closure.mli b/checker/closure.mli
index 12cee770..707a51f9 100644
--- a/checker/closure.mli
+++ b/checker/closure.mli
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: closure.mli 9902 2007-06-21 17:01:21Z herbelin $ i*)
-
 (*i*)
 open Pp
 open Names
@@ -32,6 +30,9 @@ type transparent_state = Idpred.t * Cpred.t
 val all_opaque      : transparent_state
 val all_transparent : transparent_state
 
+val is_transparent_variable : transparent_state -> variable -> bool
+val is_transparent_constant : transparent_state -> constant -> bool
+
 (* Sets of reduction kinds. *)
 module type RedFlagsSig = sig
   type reds
@@ -51,33 +52,20 @@ module type RedFlagsSig = sig
   (* Adds a reduction kind to a set *)
   val red_add : reds -> red_kind -> reds
 
-  (* Removes a reduction kind to a set *)
-  val red_sub : reds -> red_kind -> reds
-
-  (* Adds a reduction kind to a set *)
-  val red_add_transparent : reds -> transparent_state -> reds
-
   (* Build a reduction set from scratch = iter [red_add] on [no_red] *)
   val mkflags : red_kind list -> reds
 
   (* Tests if a reduction kind is set *)
   val red_set : reds -> red_kind -> bool
-
-  (* Gives the constant list *)
-  val red_get_const : reds -> bool * evaluable_global_reference list
 end
 
 module RedFlags : RedFlagsSig
 open RedFlags
 
-val beta               : reds
-val betaiota           : reds
 val betadeltaiota      : reds
 val betaiotazeta       : reds
 val betadeltaiotanolet : reds
 
-val unfold_red : evaluable_global_reference -> reds
-
 (***********************************************************************)
 type table_key =
   | ConstKey of constant
@@ -86,7 +74,6 @@ type table_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
 
 (************************************************************************)
@@ -132,23 +119,14 @@ type stack_member =
 
 and stack = stack_member list
 
-val empty_stack : stack
 val append_stack : fconstr array -> stack -> stack
-
-val decomp_stack : stack -> (fconstr * stack) option
-val array_of_stack : stack -> fconstr array
-val stack_assign : stack -> int -> fconstr -> stack
-val stack_args_size : stack -> int
-val stack_tail : int -> stack -> stack
-val stack_nth : stack -> int -> fconstr
+val eta_expand_stack : stack -> stack
 
 (* To lazy reduce a constr, create a [clos_infos] with
    [create_clos_infos], inject the term to reduce with [inject]; then use
    a reduction function *)
 
 val inject : constr -> fconstr
-(* mk_atom: prevents a term from being evaluated *)
-val mk_atom : constr -> fconstr
 
 val fterm_of : fconstr -> fterm
 val term_of_fconstr : fconstr -> constr
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 0deb80a2..890996d1 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -20,7 +20,7 @@ type polymorphic_arity = {
   poly_level : Univ.universe;
 }
 let val_pol_arity =
-  val_tuple"polyorphic_arity"[|val_list(val_opt val_univ);val_univ|]
+  val_tuple ~name:"polyorphic_arity"[|val_list(val_opt val_univ);val_univ|]
 
 type constant_type =
   | NonPolymorphicType of constr
@@ -29,256 +29,164 @@ type constant_type =
 let val_cst_type =
   val_sum "constant_type" 0 [|[|val_constr|];[|val_rctxt;val_pol_arity|]|]
 
-
-type substitution_domain =
-  | MBI of mod_bound_id
-  | MPI of module_path
-
-let val_subst_dom =
-  val_sum "substitution_domain" 0 [|[|val_uid|];[|val_mp|]|]
-
-module Umap = Map.Make(struct
-			 type t = substitution_domain
-			 let compare = Pervasives.compare
-		       end)
-
+(** Substitutions, code imported from kernel/mod_subst *)
 
 type delta_hint =
-    Inline of constr option
+  | Inline of int * constr option
   | Equiv of kernel_name
-  | Prefix_equiv of module_path
-
-type delta_key = 
-    KN of kernel_name
-  | MP of module_path
 
-module Deltamap =  Map.Make(struct 
-			      type t = delta_key
-			      let compare = Pervasives.compare
-			    end)
 
-type delta_resolver = delta_hint Deltamap.t
+module Deltamap = struct
+  type t = module_path MPmap.t * delta_hint KNmap.t
+  let empty = MPmap.empty, KNmap.empty
+  let add_kn kn hint (mm,km) = (mm,KNmap.add kn hint km)
+  let add_mp mp mp' (mm,km) = (MPmap.add mp mp' mm, km)
+  let remove_mp mp (mm,km) = (MPmap.remove mp mm, km)
+  let find_mp mp map = MPmap.find mp (fst map)
+  let find_kn kn map = KNmap.find kn (snd map)
+  let mem_mp mp map = MPmap.mem mp (fst map)
+  let mem_kn kn map = KNmap.mem kn (snd map)
+  let fold_kn f map i = KNmap.fold f (snd map) i
+  let fold fmp fkn (mm,km) i =
+    MPmap.fold fmp mm (KNmap.fold fkn km i)
+  let join map1 map2 = fold add_mp add_kn map1 map2
+end
+
+type delta_resolver = Deltamap.t
 
 let empty_delta_resolver = Deltamap.empty
 
+module MBImap = Map.Make
+  (struct
+    type t = mod_bound_id
+    let compare = Pervasives.compare
+   end)
+
+module Umap = struct
+  type 'a t = 'a MPmap.t * 'a MBImap.t
+  let empty = MPmap.empty, MBImap.empty
+  let is_empty (m1,m2) = MPmap.is_empty m1 && MBImap.is_empty m2
+  let add_mbi mbi x (m1,m2) = (m1,MBImap.add mbi x m2)
+  let add_mp mp x (m1,m2) = (MPmap.add mp x m1, m2)
+  let find_mp mp map = MPmap.find mp (fst map)
+  let find_mbi mbi map = MBImap.find mbi (snd map)
+  let mem_mp mp map = MPmap.mem mp (fst map)
+  let mem_mbi mbi map = MBImap.mem mbi (snd map)
+  let iter_mbi f map = MBImap.iter f (snd map)
+  let fold fmp fmbi (m1,m2) i =
+    MPmap.fold fmp m1 (MBImap.fold fmbi m2 i)
+  let join map1 map2 = fold add_mp add_mbi map1 map2
+end
+
 type substitution = (module_path * delta_resolver) Umap.t
 type 'a subst_fun = substitution -> 'a -> 'a
 
-let val_res_dom =
-  val_sum "delta_key" 0 [|[|val_kn|];[|val_mp|]|]
+let empty_subst = Umap.empty
 
-let val_res =
-  val_map ~name:"delta_resolver"
-    val_res_dom  
-    (val_sum "delta_hint" 0 [|[|val_opt val_constr|];[|val_kn|];[|val_mp|]|])
+let is_empty_subst = Umap.is_empty
 
-let val_subst =
-  val_map ~name:"substitution"
-    val_subst_dom (val_tuple "substition range" [|val_mp;val_res|])
+let val_delta_hint =
+  val_sum "delta_hint" 0
+    [|[|val_int; val_opt val_constr|];[|val_kn|]|]
 
+let val_res =
+  val_tuple ~name:"delta_resolver"
+    [|val_map ~name:"delta_resolver" val_mp val_mp;
+      val_map ~name:"delta_resolver" val_kn val_delta_hint|]
 
-let fold_subst fb fp =
-  Umap.fold
-    (fun k (mp,_) acc ->
-      match k with
-        | MBI mbid -> fb mbid mp acc
-        | MPI mp1 -> fp mp1 mp acc)
+let val_mp_res = val_tuple [|val_mp;val_res|]
 
-let empty_subst = Umap.empty
+let val_subst =
+  val_tuple ~name:"substitution"
+    [|val_map ~name:"substitution" val_mp val_mp_res;
+      val_map ~name:"substitution" val_uid val_mp_res|]
 
-let add_mbid mbid mp =
-  Umap.add (MBI mbid) (mp,empty_delta_resolver)
-let add_mp mp1 mp2  =
-  Umap.add (MPI mp1) (mp2,empty_delta_resolver)
+let add_mbid mbid mp = Umap.add_mbi mbid (mp,empty_delta_resolver)
+let add_mp mp1 mp2 = Umap.add_mp mp1 (mp2,empty_delta_resolver)
 
 let map_mbid mbid mp = add_mbid mbid mp empty_subst
 let map_mp mp1 mp2 = add_mp mp1 mp2 empty_subst
 
-let add_inline_delta_resolver con =
-  Deltamap.add (KN(user_con con)) (Inline None)
-    
-let add_inline_constr_delta_resolver con cstr =
-  Deltamap.add (KN(user_con con)) (Inline (Some cstr))
-
-let add_constant_delta_resolver con =
-  Deltamap.add (KN(user_con con)) (Equiv (canonical_con con))
-
-let add_mind_delta_resolver mind =
-  Deltamap.add (KN(user_mind mind)) (Equiv (canonical_mind mind))
-
-let add_mp_delta_resolver mp1 mp2 = 
-  Deltamap.add (MP mp1) (Prefix_equiv mp2)
-
-let mp_in_delta mp = 
-  Deltamap.mem (MP mp) 
-
-let con_in_delta con resolver = 
-try 
-  match Deltamap.find (KN(user_con con)) resolver with
-  | Inline _  | Prefix_equiv _ -> false
-  | Equiv _ -> true
-with
- Not_found -> false
-
-let mind_in_delta mind resolver = 
-try 
-  match Deltamap.find (KN(user_mind mind)) resolver with
-  | Inline _  | Prefix_equiv _ -> false
-  | Equiv _ -> true
-with
- Not_found -> false
-
-let delta_of_mp resolve mp =
-  try 
-    match Deltamap.find (MP mp) resolve with
-      | Prefix_equiv mp1 -> mp1
-      | _ -> anomaly "mod_subst: bad association in delta_resolver"
-  with
-      Not_found -> mp
-	
-let delta_of_kn resolve kn =
-  try 
-    match Deltamap.find (KN kn) resolve with
-      | Equiv kn1 -> kn1
-      | Inline _ -> kn
-      | _ -> anomaly 
-	  "mod_subst: bad association in delta_resolver"
-  with
-      Not_found -> kn
-
-let remove_mp_delta_resolver resolver mp =
-    Deltamap.remove (MP mp) resolver
-
-exception Inline_kn
+let mp_in_delta mp =
+  Deltamap.mem_mp mp
 
-let rec find_prefix resolve mp = 
+let rec find_prefix resolve mp =
   let rec sub_mp = function
-    | MPdot(mp,l) as mp_sup -> 
-	(try 
-	   match Deltamap.find (MP mp_sup) resolve with
-	     | Prefix_equiv mp1 -> mp1
-	     | _ -> anomaly 
-		 "mod_subst: bad association in delta_resolver"
-	 with
-	     Not_found -> MPdot(sub_mp mp,l))
-    | p -> 
-	match Deltamap.find (MP p) resolve with
-	  | Prefix_equiv mp1 -> mp1
-	  | _ -> anomaly 
-		 "mod_subst: bad association in delta_resolver"	
+    | MPdot(mp,l) as mp_sup ->
+	(try Deltamap.find_mp mp_sup resolve
+	 with Not_found -> MPdot(sub_mp mp,l))
+    | p -> Deltamap.find_mp p resolve
   in
-    try 
-      sub_mp mp
-    with
-	Not_found -> mp
-	  
+  try sub_mp mp with Not_found -> mp
+
+(** Nota: the following function is slightly different in mod_subst
+    PL: Is it on purpose ? *)
+
 let solve_delta_kn resolve kn =
-  try 
-      match Deltamap.find (KN kn) resolve with
-	| Equiv kn1 -> kn1
-	| Inline _ -> raise Inline_kn
-	| _ -> anomaly 
-	    "mod_subst: bad association in delta_resolver"
-  with
-      Not_found | Inline_kn -> 
-	let mp,dir,l = repr_kn kn in
-	let new_mp = find_prefix resolve mp in
-	  if mp == new_mp then 
-	    kn
-	  else
-	    make_kn new_mp dir l
-	      
+  try
+    match Deltamap.find_kn kn resolve with
+      | Equiv kn1 -> kn1
+      | Inline _ -> raise Not_found
+  with Not_found ->
+    let mp,dir,l = repr_kn kn in
+    let new_mp = find_prefix resolve mp in
+    if mp == new_mp then
+      kn
+    else
+      make_kn new_mp dir l
+
+let gen_of_delta resolve x kn fix_can =
+  try
+    let new_kn = solve_delta_kn resolve kn in
+    if kn == new_kn then x else fix_can new_kn
+  with _ -> x
 
 let constant_of_delta resolve con =
   let kn = user_con con in
-  let new_kn = solve_delta_kn resolve kn in
-    if kn == new_kn then
-      con
-    else
-      constant_of_kn_equiv kn new_kn
-	
+  gen_of_delta resolve con kn (constant_of_kn_equiv kn)
+
 let constant_of_delta2 resolve con =
-  let kn = canonical_con con in
-  let kn1 = user_con con in
-  let new_kn = solve_delta_kn resolve kn in
-    if kn == new_kn then
-      con
-    else
-      constant_of_kn_equiv kn1 new_kn
+  let kn, kn' = canonical_con con, user_con con in
+  gen_of_delta resolve con kn (constant_of_kn_equiv kn')
 
 let mind_of_delta resolve mind =
   let kn = user_mind mind in
-  let new_kn = solve_delta_kn resolve kn in
-    if kn == new_kn then
-      mind
-    else
-      mind_of_kn_equiv kn new_kn
-	
-let mind_of_delta2 resolve mind =
-  let kn = canonical_mind mind in
-  let kn1 = user_mind mind in
-  let new_kn = solve_delta_kn resolve kn in
-    if kn == new_kn then
-      mind
-    else
-      mind_of_kn_equiv kn1 new_kn
-
+  gen_of_delta resolve mind kn (mind_of_kn_equiv kn)
 
+let mind_of_delta2 resolve mind =
+  let kn, kn' = canonical_mind mind, user_mind mind in
+  gen_of_delta resolve mind kn (mind_of_kn_equiv kn')
 
-let inline_of_delta resolver = 
-  let extract key hint l =
-    match key,hint with 
-      |KN kn, Inline _ -> kn::l
-      | _,_ -> l
-  in
-    Deltamap.fold extract resolver []
+let find_inline_of_delta kn resolve =
+  match Deltamap.find_kn kn resolve with
+    | Inline (_,o) -> o
+    | _ -> raise Not_found
 
-exception Not_inline
-  
 let constant_of_delta_with_inline resolve con =
   let kn1,kn2 = canonical_con con,user_con con in
-    try
-      match Deltamap.find (KN kn2) resolve with 
-	| Inline None -> None
-	| Inline (Some const) -> Some const
-	| _ -> raise Not_inline
-    with
-	Not_found | Not_inline -> 
-	  try match Deltamap.find (KN kn1) resolve with 
-	    | Inline None -> None
-	    | Inline (Some const) -> Some const
-	    | _ -> raise Not_inline
-	  with
-	      Not_found | Not_inline -> None
+  try find_inline_of_delta kn2 resolve
+  with Not_found ->
+    try find_inline_of_delta kn1 resolve
+    with Not_found -> None
 
 let subst_mp0 sub mp = (* 's like subst *)
  let rec aux mp =
   match mp with
-    | MPfile sid -> 
-        let mp',resolve = Umap.find (MPI (MPfile sid)) sub in
-         mp',resolve
+    | MPfile sid -> Umap.find_mp mp sub
     | MPbound bid ->
 	begin
-	  try
-            let mp',resolve = Umap.find (MBI bid) sub in
-              mp',resolve
-	  with Not_found ->
-	    let mp',resolve = Umap.find (MPI mp) sub in
-              mp',resolve
+	  try Umap.find_mbi bid sub
+	  with Not_found -> Umap.find_mp mp sub
 	end
     | MPdot (mp1,l) as mp2 ->
 	begin
-	  try
-	    let mp',resolve = Umap.find (MPI mp2) sub in
-              mp',resolve
+	  try Umap.find_mp mp2 sub
 	  with Not_found ->
 	    let mp1',resolve = aux mp1 in
-	      MPdot (mp1',l),resolve
+	    MPdot (mp1',l),resolve
 	end
  in
-  try
-    Some (aux mp)
-  with Not_found -> None
+ try Some (aux mp) with Not_found -> None
 
 let subst_mp sub mp =
  match subst_mp0 sub mp with
@@ -305,127 +213,58 @@ type sideconstantsubst =
   | User
   | Canonical
 
+
+let gen_subst_mp f sub mp1 mp2 =
+  match subst_mp0 sub mp1, subst_mp0 sub mp2 with
+    | None, None -> raise No_subst
+    | Some (mp',resolve), None -> User, (f mp' mp2), resolve
+    | None, Some (mp',resolve) -> Canonical, (f mp1 mp'), resolve
+    | Some (mp1',_), Some (mp2',resolve2) -> Canonical, (f mp1' mp2'), resolve2
+
 let subst_ind sub mind =
-  let kn1,kn2 = user_mind mind,canonical_mind mind in
+  let kn1,kn2 = user_mind mind, canonical_mind mind in
   let mp1,dir,l = repr_kn kn1 in
   let mp2,_,_ = repr_kn kn2 in
-    try 
-      let side,mind',resolve =   
-        match subst_mp0 sub mp1,subst_mp0 sub mp2 with
-	    None,None ->raise No_subst
-	  | Some (mp',resolve),None -> User,(make_mind_equiv mp' mp2 dir l), resolve
-	  | None, Some(mp',resolve)-> Canonical,(make_mind_equiv mp1 mp' dir l), resolve
-	  | Some(mp1',resolve1),Some(mp2',resolve2)->Canonical,
-	      (make_mind_equiv mp1' mp2' dir l), resolve2 
-      in
-	match side with
-	  |User ->
-	     let mind = mind_of_delta resolve mind' in
-	       mind
-	  |Canonical ->
-	     let mind = mind_of_delta2 resolve mind' in
-	       mind
-    with 
-	No_subst -> mind
-
-let subst_mind0 sub mind =
-  let kn1,kn2 = user_mind mind,canonical_mind mind in
-  let mp1,dir,l = repr_kn kn1 in
-  let mp2,_,_ = repr_kn kn2 in
-    try 
-      let side,mind',resolve =   
-        match subst_mp0 sub mp1,subst_mp0 sub mp2 with
-	    None,None ->raise No_subst
-	  | Some (mp',resolve),None -> User,(make_mind_equiv mp' mp2 dir l), resolve
-	  | None, Some(mp',resolve)-> Canonical,(make_mind_equiv mp1 mp' dir l), resolve
-	  | Some(mp1',resolve1),Some(mp2',resolve2)->Canonical,
-	      (make_mind_equiv mp1' mp2' dir l), resolve2
-      in
-	match side with
-	  |User ->
-	     let mind = mind_of_delta resolve mind' in
-	       Some mind
-	  |Canonical ->
-	     let mind = mind_of_delta2 resolve mind' in
-	       Some mind
-    with 
-	No_subst -> Some mind
-
-let subst_con sub con =
-  let kn1,kn2 = user_con con,canonical_con con in
-  let mp1,dir,l = repr_kn kn1 in
-  let mp2,_,_ = repr_kn kn2 in
-    try 
-      let side,con',resolve =   
-        match subst_mp0 sub mp1,subst_mp0 sub mp2 with
-	    None,None ->raise No_subst
-	  | Some (mp',resolve),None -> User,(make_con_equiv mp' mp2 dir l), resolve
-	  | None, Some(mp',resolve)-> Canonical,(make_con_equiv mp1 mp' dir l), resolve
-	  | Some(mp1',resolve1),Some(mp2',resolve2)->Canonical,
-	      (make_con_equiv mp1' mp2' dir l), resolve2 
-      in
-	match constant_of_delta_with_inline resolve con' with
-            None -> begin
-	      match side with
-	      |User ->
-	      let con = constant_of_delta resolve con' in
-		con,Const con
-	      |Canonical ->
-		  let con = constant_of_delta2 resolve con' in
-		con,Const con
-	    end
-	  | Some t -> con',t
-    with No_subst -> con , Const con 
- 
+  let rebuild_mind mp1 mp2 = make_mind_equiv mp1 mp2 dir l in
+  try
+    let side,mind',resolve = gen_subst_mp rebuild_mind sub mp1 mp2 in
+    match side with
+      | User -> mind_of_delta resolve mind'
+      | Canonical -> mind_of_delta2 resolve mind'
+  with No_subst -> mind
 
 let subst_con0 sub con =
   let kn1,kn2 = user_con con,canonical_con con in
   let mp1,dir,l = repr_kn kn1 in
   let mp2,_,_ = repr_kn kn2 in
-    try  
-      let side,con',resolve =   
-	match subst_mp0 sub mp1,subst_mp0 sub mp2 with
-	    None,None ->raise No_subst
-	  | Some (mp',resolve),None -> User,(make_con_equiv mp' mp2 dir l), resolve
-	  | None, Some(mp',resolve)-> Canonical,(make_con_equiv mp1 mp' dir l), resolve
-	  | Some(mp1',resolve1),Some(mp2',resolve2)->Canonical,
-	      (make_con_equiv mp1' mp2' dir l), resolve2 
+  let rebuild_con mp1 mp2 = make_con_equiv mp1 mp2 dir l in
+  let dup con = con, Const con in
+  let side,con',resolve = gen_subst_mp rebuild_con sub mp1 mp2 in
+  match constant_of_delta_with_inline resolve con' with
+    | Some t -> con', t
+    | None ->
+      let con'' = match side with
+	| User -> constant_of_delta resolve con'
+	| Canonical -> constant_of_delta2 resolve con'
       in
-	match constant_of_delta_with_inline resolve con' with
-	    None ->begin
-	      match side with
-	      |User ->
-	      let con = constant_of_delta resolve con' in
-		Some (Const con)
-	      |Canonical ->
-		  let con = constant_of_delta2 resolve con' in
-		Some (Const con)
-	    end
-	  | t ->  t
-    with No_subst -> Some (Const con)
-
+      if con'' == con then raise No_subst else dup con''
 
 let rec map_kn f f' c =
   let func = map_kn f f' in
     match c with
-      | Const kn ->
-	  (match f' kn with
-	       None -> c
-	     | Some const ->const)
+      | Const kn -> (try snd (f' kn) with No_subst -> c)
       | Ind (kn,i) ->
-         (match f kn with
-             None -> c
-           | Some kn' ->
-	      Ind (kn',i))
+	  let kn' = f kn in
+	  if kn'==kn then c else Ind (kn',i)
       | Construct ((kn,i),j) ->
-         (match f kn with
-             None -> c
-           | Some kn' ->
-	       Construct ((kn',i),j))
+	  let kn' = f kn in
+	  if kn'==kn then c else Construct ((kn',i),j)
       | Case (ci,p,ct,l) ->
 	  let ci_ind =
             let (kn,i) = ci.ci_ind in
-              (match f kn with None -> ci.ci_ind | Some kn' -> kn',i ) in
+	    let kn' = f kn in
+	    if kn'==kn then ci.ci_ind else kn',i
+	  in
 	  let p' = func p in
 	  let ct' = func ct in
 	  let l' = array_smartmap func l in
@@ -476,8 +315,9 @@ let rec map_kn f f' c =
 	    else CoFix (ln,(lna,tl',bl'))
       | _ -> c
 
-let subst_mps sub =
-  map_kn (subst_mind0 sub) (subst_con0 sub)
+let subst_mps sub c =
+  if is_empty_subst sub then c
+  else map_kn (subst_ind sub) (subst_con0 sub) c
 
 
 type 'a lazy_subst =
@@ -507,125 +347,113 @@ let rec mp_in_mp mp mp1 =
     | _ when mp1 = mp -> true
     | MPdot (mp2,l) -> mp_in_mp mp mp2
     | _ -> false
-	
-let mp_in_key mp key = 
-  match key with
-    | MP mp1 -> 
-	mp_in_mp mp mp1
-    | KN kn -> 
-	let mp1,dir,l = repr_kn kn in
-	  mp_in_mp mp mp1
-  
+
 let subset_prefixed_by mp resolver =
-  let prefixmp key hint resolv =
-    if mp_in_key mp key then
-      Deltamap.add key hint resolv
-    else 
-      resolv
+  let mp_prefix mkey mequ rslv =
+    if mp_in_mp mp mkey then Deltamap.add_mp mkey mequ rslv else rslv
+  in
+  let kn_prefix kn hint rslv =
+    match hint with
+      | Inline _ -> rslv
+      | Equiv _ ->
+	if mp_in_mp mp (modpath kn) then Deltamap.add_kn kn hint rslv else rslv
   in
-    Deltamap.fold prefixmp resolver empty_delta_resolver
+  Deltamap.fold mp_prefix kn_prefix resolver empty_delta_resolver
 
 let subst_dom_delta_resolver subst resolver =
-  let apply_subst key hint resolver =
-    match key with
-	(MP mp) ->
-	  Deltamap.add (MP (subst_mp subst mp)) hint resolver
-      | (KN kn) ->
-	  Deltamap.add (KN (subst_kn subst kn)) hint resolver
+  let mp_apply_subst mkey mequ rslv =
+    Deltamap.add_mp (subst_mp subst mkey) mequ rslv
   in
-    Deltamap.fold apply_subst resolver empty_delta_resolver
+  let kn_apply_subst kkey hint rslv =
+    Deltamap.add_kn (subst_kn subst kkey) hint rslv
+  in
+  Deltamap.fold mp_apply_subst kn_apply_subst resolver empty_delta_resolver
 
-let subst_mp_delta sub mp key=
+let subst_mp_delta sub mp mkey =
  match subst_mp0 sub mp with
     None -> empty_delta_resolver,mp
-  | Some (mp',resolve) -> 
+  | Some (mp',resolve) ->
       let mp1 = find_prefix resolve mp' in
       let resolve1 = subset_prefixed_by mp1 resolve in
-	match key with
-	    MP mpk ->
-	      (subst_dom_delta_resolver 
-		 (map_mp mp1 mpk) resolve1),mp1
-	  | _ -> anomaly "Mod_subst: Bad association in resolver" 
-
-let subst_codom_delta_resolver subst resolver =
-  let apply_subst key hint resolver =
-    match hint with
-	Prefix_equiv mp ->
-	  let derived_resolve,mpnew = subst_mp_delta subst mp key in
-	    Deltamap.fold Deltamap.add derived_resolve
-	      (Deltamap.add key (Prefix_equiv mpnew) resolver)
-      | (Equiv kn) ->
-	  Deltamap.add key (Equiv (subst_kn_delta subst kn)) resolver
-      | Inline None ->
-	  Deltamap.add key hint resolver
-      | Inline (Some t) ->
-	  Deltamap.add key (Inline (Some (subst_mps subst t))) resolver
+      (subst_dom_delta_resolver
+	 (map_mp mp1 mkey) resolve1),mp1
+
+let gen_subst_delta_resolver dom subst resolver =
+  let mp_apply_subst mkey mequ rslv =
+    let mkey' = if dom then subst_mp subst mkey else mkey in
+    let rslv',mequ' = subst_mp_delta subst mequ mkey in
+    Deltamap.join rslv' (Deltamap.add_mp mkey' mequ' rslv)
   in
-    Deltamap.fold apply_subst resolver empty_delta_resolver
+  let kn_apply_subst kkey hint rslv =
+    let kkey' = if dom then subst_kn subst kkey else kkey in
+    let hint' = match hint with
+      | Equiv kequ -> Equiv (subst_kn_delta subst kequ)
+      | Inline (lev,Some t) -> Inline (lev,Some (subst_mps subst t))
+      | Inline (_,None) -> hint
+    in
+    Deltamap.add_kn kkey' hint' rslv
+  in
+  Deltamap.fold mp_apply_subst kn_apply_subst resolver empty_delta_resolver
+
+let subst_codom_delta_resolver = gen_subst_delta_resolver false
+let subst_dom_codom_delta_resolver = gen_subst_delta_resolver true
 
-let subst_dom_codom_delta_resolver subst resolver =
-  subst_dom_delta_resolver subst
-    (subst_codom_delta_resolver subst resolver)
-    
 let update_delta_resolver resolver1 resolver2 =
- let apply_res key hint res = 
-      try
-	match hint with
-	    Prefix_equiv mp ->
-	      let new_hint =
-		Prefix_equiv (find_prefix resolver2 mp)
-	      in Deltamap.add key new_hint res
-	  | Equiv kn ->
-	      let new_hint =
-		Equiv (solve_delta_kn resolver2 kn)
-	      in Deltamap.add key new_hint res
-	  | _ -> Deltamap.add key hint res
-      with Not_found ->
-	Deltamap.add key hint res
-    in
-      Deltamap.fold apply_res resolver1 empty_delta_resolver
+  let mp_apply_rslv mkey mequ rslv =
+    if Deltamap.mem_mp mkey resolver2 then rslv
+    else Deltamap.add_mp mkey (find_prefix resolver2 mequ) rslv
+  in
+  let kn_apply_rslv kkey hint rslv =
+    if Deltamap.mem_kn kkey resolver2 then rslv
+    else
+      let hint' = match hint with
+	| Equiv kequ -> Equiv (solve_delta_kn resolver2 kequ)
+	| _ -> hint
+      in
+      Deltamap.add_kn kkey hint' rslv
+  in
+  Deltamap.fold mp_apply_rslv kn_apply_rslv resolver1 empty_delta_resolver
 
 let add_delta_resolver resolver1 resolver2 =
   if resolver1 == resolver2 then
     resolver2
+  else if resolver2 = empty_delta_resolver then
+    resolver1
   else
-    Deltamap.fold Deltamap.add (update_delta_resolver resolver1 resolver2)
-      resolver2
+    Deltamap.join (update_delta_resolver resolver1 resolver2) resolver2
 
 let substition_prefixed_by k mp subst =
-  let prefixmp key (mp_to,reso) sub =
-    match key with 
-      | MPI mpk ->
-	  if mp_in_mp mp mpk && mp <> mpk then
-	    let new_key = replace_mp_in_mp mp k mpk in
-	      Umap.add (MPI new_key) (mp_to,reso) sub
-	  else 
-	    sub
-      |  _ -> sub
+  let mp_prefixmp kmp (mp_to,reso) sub =
+    if mp_in_mp mp kmp && mp <> kmp then
+      let new_key = replace_mp_in_mp mp k kmp in
+      Umap.add_mp new_key (mp_to,reso) sub
+    else sub
+  in
+  let mbi_prefixmp mbi _ sub = sub
   in
-    Umap.fold prefixmp subst empty_subst
+  Umap.fold mp_prefixmp mbi_prefixmp subst empty_subst
 
-let join (subst1 : substitution) (subst2 : substitution) =
-  let apply_subst key (mp,resolve) res =
+let join subst1 subst2 =
+  let apply_subst mpk add (mp,resolve) res =
     let mp',resolve' =
       match subst_mp0 subst2 mp with
-	  None -> mp, None
-	| Some (mp',resolve') ->  mp'
-	    ,Some resolve' in
-    let resolve'' : delta_resolver =
+	| None -> mp, None
+	| Some (mp',resolve') ->  mp', Some resolve' in
+    let resolve'' =
       match resolve' with
-          Some res -> 
-	    add_delta_resolver 
+        | Some res ->
+	    add_delta_resolver
 	      (subst_dom_codom_delta_resolver subst2 resolve) res
-	| None -> 
+	| None ->
 	    subst_codom_delta_resolver subst2 resolve
     in
-    let k = match key with MBI mp -> MPbound mp | MPI mp -> mp in
-    let prefixed_subst = substition_prefixed_by k mp subst2 in
-      Umap.fold Umap.add prefixed_subst 
-	(Umap.add key (mp',resolve'') res) in
-  let subst = Umap.fold apply_subst subst1 empty_subst in
-    (Umap.fold Umap.add subst2 subst) 
+    let prefixed_subst = substition_prefixed_by mpk mp' subst2 in
+    Umap.join prefixed_subst (add (mp',resolve'') res)
+  in
+  let mp_apply_subst mp = apply_subst mp (Umap.add_mp mp) in
+  let mbi_apply_subst mbi = apply_subst (MPbound mbi) (Umap.add_mbi mbi) in
+  let subst = Umap.fold mp_apply_subst mbi_apply_subst subst1 empty_subst in
+  Umap.join subst2 subst
 
 let force fsubst r =
   match !r with
@@ -650,25 +478,67 @@ let val_cstr_subst = val_substituted val_constr
 
 let subst_constr_subst = subst_substituted
 
+(** Beware! In .vo files, lazy_constr are stored as integers
+   used as indexes for a separate table. The actual lazy_constr is restored
+   later, by [Safe_typing.LightenLibrary.load]. This allows us
+   to use here a different definition of lazy_constr than coqtop:
+   since the checker will inspect all proofs parts, even opaque
+   ones, no need to use Lazy.t here *)
+
+type lazy_constr = constr_substituted
+let subst_lazy_constr = subst_substituted
+let force_lazy_constr = force_constr
+let lazy_constr_from_val c = c
+let val_lazy_constr = val_cstr_subst
+
+(** Inlining level of parameters at functor applications.
+    This is ignored by the checker. *)
+
+type inline = int option
+
+(** A constant can have no body (axiom/parameter), or a
+    transparent body, or an opaque one *)
+
+type constant_def =
+  | Undef of inline
+  | Def of constr_substituted
+  | OpaqueDef of lazy_constr
+
+let val_cst_def =
+  val_sum "constant_def" 0
+    [|[|val_opt val_int|]; [|val_cstr_subst|]; [|val_lazy_constr|]|]
+
+let subst_constant_def sub = function
+  | Undef inl -> Undef inl
+  | Def c -> Def (subst_constr_subst sub c)
+  | OpaqueDef lc -> OpaqueDef (subst_lazy_constr sub lc)
+
 type constant_body = {
     const_hyps : section_context; (* New: younger hyp at top *)
-    const_body : constr_substituted option;
+    const_body : constant_def;
     const_type : constant_type;
     const_body_code : to_patch_substituted;
-   (* const_type_code : Cemitcodes.to_patch; *)
-    const_constraints : Univ.constraints;
-    const_opaque : bool;
-    const_inline : bool}
+    const_constraints : Univ.constraints }
 
-let val_cb = val_tuple "constant_body"
+let body_of_constant cb = match cb.const_body with
+  | Undef _ -> None
+  | Def c -> Some c
+  | OpaqueDef c -> Some c
+
+let constant_has_body cb = match cb.const_body with
+  | Undef _ -> false
+  | Def _ | OpaqueDef _ -> true
+
+let is_opaque cb = match cb.const_body with
+  | OpaqueDef _ -> true
+  | Def _ | Undef _ -> false
+
+let val_cb = val_tuple ~name:"constant_body"
   [|val_nctxt;
-    val_opt val_cstr_subst;
+    val_cst_def;
     val_cst_type;
     no_val;
-    val_cstrs;
-    val_bool;
-    val_bool |]
-
+    val_cstrs|]
 
 let subst_rel_declaration sub (id,copt,t as x) =
   let copt' = Option.smartmap (subst_mps sub) copt in
@@ -679,14 +549,14 @@ let subst_rel_context sub = list_smartmap (subst_rel_declaration sub)
 
 type recarg =
   | Norec
-  | Mrec of int
+  | Mrec of inductive
   | Imbr of inductive
 let val_recarg = val_sum "recarg" 1 (* Norec *)
-  [|[|val_int|] (* Mrec *);[|val_ind|] (* Imbr *)|]
+  [|[|val_ind|] (* Mrec *);[|val_ind|] (* Imbr *)|]
 
 let subst_recarg sub r = match r with
-  | Norec | Mrec _  -> r
-  | Imbr (kn,i) -> let kn' = subst_ind sub kn in
+  | Norec  -> r
+  | (Mrec(kn,i)|Imbr (kn,i)) -> let kn' = subst_ind sub kn in
       if kn==kn' then r else Imbr (kn',i)
 
 type wf_paths = recarg Rtree.t
@@ -724,7 +594,7 @@ type monomorphic_inductive_arity = {
   mind_sort : sorts;
 }
 let val_mono_ind_arity =
-  val_tuple"monomorphic_inductive_arity"[|val_constr;val_sort|]
+  val_tuple ~name:"monomorphic_inductive_arity"[|val_constr;val_sort|]
 
 type inductive_arity =
 | Monomorphic of monomorphic_inductive_arity
@@ -784,7 +654,7 @@ type one_inductive_body = {
     mind_reloc_tbl :  reloc_table;
   }
 
-let val_one_ind = val_tuple "one_inductive_body"
+let val_one_ind = val_tuple ~name:"one_inductive_body"
   [|val_id;val_rctxt;val_ind_arity;val_array val_id;val_array val_constr;
     val_int;val_int;val_list val_sortfam;val_array val_constr;val_array val_int;
     val_wfp;val_int;val_int;no_val|]
@@ -820,7 +690,7 @@ type mutual_inductive_body = {
     mind_constraints : Univ.constraints;
 
   }
-let val_ind_pack = val_tuple "mutual_inductive_body"
+let val_ind_pack = val_tuple ~name:"mutual_inductive_body"
   [|val_array val_one_ind;val_bool;val_bool;val_int;val_nctxt;
     val_int; val_int; val_rctxt;val_cstrs|]
 
@@ -832,13 +702,10 @@ let subst_arity sub = function
 (* TODO: should be changed to non-coping after Term.subst_mps *)
 let subst_const_body sub cb = {
     const_hyps = (assert (cb.const_hyps=[]); []);
-    const_body = Option.map (subst_constr_subst sub) cb.const_body;
+    const_body = subst_constant_def sub cb.const_body;
     const_type = subst_arity sub cb.const_type;
     const_body_code = (*Cemitcodes.subst_to_patch_subst sub*) cb.const_body_code;
-    (*const_type_code = Cemitcodes.subst_to_patch sub cb.const_type_code;*)
-    const_constraints = cb.const_constraints;
-    const_opaque = cb.const_opaque;
-    const_inline = cb.const_inline}
+    const_constraints = cb.const_constraints}
 
 let subst_arity sub = function
 | Monomorphic s ->
@@ -923,7 +790,7 @@ let rec val_sfb o = val_sum "struct_field_body" 0
     [|val_module|];   (* SFBmodule *)
     [|val_modtype|]   (* SFBmodtype *)
   |] o
-and val_sb o = val_list (val_tuple"label*sfb"[|val_id;val_sfb|]) o
+and val_sb o = val_list (val_tuple ~name:"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 *)
@@ -934,10 +801,10 @@ and val_seb o = val_sum "struct_expr_body" 0
 and val_with o = val_sum "with_declaration_body" 0
   [|[|val_list val_id;val_mp|];
     [|val_list val_id;val_cb|]|] o
-and val_module o = val_tuple "module_body"
+and val_module o = val_tuple ~name:"module_body"
   [|val_mp;val_opt val_seb;val_seb;
     val_opt val_seb;val_cstrs;val_res;no_val|] o
-and val_modtype o = val_tuple "module_type_body"
+and val_modtype o = val_tuple ~name:"module_type_body"
   [|val_mp;val_seb;val_opt val_seb;val_cstrs;val_res|] o
 
 
diff --git a/checker/declarations.mli b/checker/declarations.mli
index b39fd6f2..90beb326 100644
--- a/checker/declarations.mli
+++ b/checker/declarations.mli
@@ -29,26 +29,53 @@ type constr_substituted
 val force_constr : constr_substituted -> constr
 val from_val : constr -> constr_substituted
 
+(** Beware! In .vo files, lazy_constr are stored as integers
+   used as indexes for a separate table. The actual lazy_constr is restored
+   later, by [Safe_typing.LightenLibrary.load]. This allows us
+   to use here a different definition of lazy_constr than coqtop:
+   since the checker will inspect all proofs parts, even opaque
+   ones, no need to use Lazy.t here *)
+
+type lazy_constr
+val force_lazy_constr : lazy_constr -> constr
+val lazy_constr_from_val : constr_substituted -> lazy_constr
+
+(** Inlining level of parameters at functor applications.
+    This is ignored by the checker. *)
+
+type inline = int option
+
+(** A constant can have no body (axiom/parameter), or a
+    transparent body, or an opaque one *)
+
+type constant_def =
+  | Undef of inline
+  | Def of constr_substituted
+  | OpaqueDef of lazy_constr
+
 type constant_body = {
     const_hyps : section_context; (* New: younger hyp at top *)
-    const_body : constr_substituted option;
+    const_body : constant_def;
     const_type : constant_type;
     const_body_code : to_patch_substituted;
-    const_constraints : Univ.constraints;
-    const_opaque : bool;
-    const_inline : bool}
+    const_constraints : Univ.constraints }
+
+val body_of_constant : constant_body -> constr_substituted option
+val constant_has_body : constant_body -> bool
+val is_opaque : constant_body -> bool
 
 (* Mutual inductives *)
 
 type recarg =
   | Norec
-  | Mrec of int
+  | Mrec of inductive
   | Imbr of inductive
 
 type wf_paths = recarg Rtree.t
 
 val mk_norec : wf_paths
 val mk_paths : recarg -> wf_paths list array -> wf_paths
+val dest_recarg : wf_paths -> recarg
 val dest_subterms : wf_paths -> wf_paths list array
 
 type monomorphic_inductive_arity = {
@@ -186,11 +213,6 @@ and module_type_body =
 
 (* Substitutions *)
 
-val fold_subst :
-  (mod_bound_id -> module_path -> 'a -> 'a) ->
-  (module_path -> module_path -> 'a -> 'a) ->
-  substitution -> 'a -> 'a
-
 type 'a subst_fun = substitution -> 'a -> 'a
 
 val empty_subst : substitution
@@ -211,6 +233,6 @@ val subst_module : substitution -> module_body -> module_body
 val join : substitution -> substitution -> substitution
 
 (* Validation *)
-val val_eng : Obj.t -> unit
-val val_module : Obj.t -> unit
-val val_modtype : Obj.t -> unit
+val val_eng : Validate.func
+val val_module : Validate.func
+val val_modtype : Validate.func
diff --git a/checker/environ.ml b/checker/environ.ml
index f7dd46f8..99b36457 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -98,7 +98,7 @@ let named_type id env =
 
 (* Universe constraints *)
 let add_constraints c env =
-  if c == Constraint.empty then
+  if c == empty_constraint then
     env
   else
     let s = env.env_stratification in
@@ -121,25 +121,16 @@ let add_constant kn cs env =
 	env_constants = new_constants } in
   { env with env_globals = new_globals }
 
-(* constant_type gives the type of a constant *)
-let constant_type env kn =
-  let cb = lookup_constant kn env in
-  cb.const_type
-
 type const_evaluation_result = NoBody | Opaque
 
 exception NotEvaluableConst of const_evaluation_result
 
 let constant_value env kn =
   let cb = lookup_constant kn env in
-  if cb.const_opaque then raise (NotEvaluableConst Opaque);
   match cb.const_body with
-    | Some l_body -> force_constr l_body
-    | None -> raise (NotEvaluableConst NoBody)
-
-let constant_opt_value env cst =
-  try Some (constant_value env cst)
-  with NotEvaluableConst _ -> None
+    | Def l_body -> force_constr l_body
+    | OpaqueDef _ -> raise (NotEvaluableConst Opaque)
+    | Undef _ -> raise (NotEvaluableConst NoBody)
 
 (* A global const is evaluable if it is defined and not opaque *)
 let evaluable_constant cst env =
diff --git a/checker/environ.mli b/checker/environ.mli
index ea446cdb..628febbb 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -50,11 +50,9 @@ 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
 type const_evaluation_result = NoBody | Opaque
 exception NotEvaluableConst of const_evaluation_result
 val constant_value : env -> constant -> constr
-val constant_opt_value : env -> constant -> constr option
 val evaluable_constant : constant -> env -> bool
 
 (* Inductives *)
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 277fed30..1e773df6 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: indtypes.ml 10296 2007-11-07 11:02:42Z barras $ *)
-
 open Util
 open Names
 open Univ
@@ -178,7 +176,7 @@ let check_predicativity env s small level =
       Type u, _ ->
         let u' = fresh_local_univ () in
         let cst =
-          merge_constraints (enforce_geq u' u Constraint.empty)
+          merge_constraints (enforce_geq u' u empty_constraint)
             (universes env) in
         if not (check_geq cst u' level) then
           failwith "impredicative Type inductive type"
@@ -394,7 +392,7 @@ let rec ienv_decompose_prod (env,_,_,_ as ienv) n c =
 
 (* The recursive function that checks positivity and builds the list
    of recursive arguments *)
-let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp i indlc =
+let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc =
   let lparams = rel_context_length hyps in
   (* check the inductive types occur positively in [c] *)
   let rec check_pos (env, n, ntypes, ra_env as ienv) c =
@@ -496,7 +494,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp i indlc =
           with IllFormedInd err ->
             explain_ind_err (ntypes-i) env lparams c err)
       indlc
-  in mk_paths (Mrec i) irecargs
+  in mk_paths (Mrec ind) irecargs
 
 let check_subtree (t1:'a) (t2:'a) =
   if not (Rtree.compare_rtree (fun t1 t2 ->
@@ -507,16 +505,17 @@ let check_subtree (t1:'a) (t2:'a) =
     failwith "bad recursive trees"
 (* if t1=t2 then () else msg_warning (str"TODO: check recursive positions")*)
 
-let check_positivity env_ar params nrecp inds =
+let check_positivity env_ar mind params nrecp inds =
   let ntypes = Array.length inds in
-  let rc = Array.mapi (fun j t -> (Mrec j,t)) (Rtree.mk_rec_calls ntypes) in
+  let rc =
+    Array.mapi (fun j t -> (Mrec(mind,j),t)) (Rtree.mk_rec_calls ntypes) in
   let lra_ind = List.rev (Array.to_list rc) in
   let lparams = rel_context_length params in
   let check_one i mip =
     let ra_env =
       list_tabulate (fun _ -> (Norec,mk_norec)) lparams @ lra_ind in
     let ienv = (env_ar, 1+lparams, ntypes, ra_env) in
-      check_positivity_one ienv params nrecp i mip.mind_nf_lc
+      check_positivity_one ienv params nrecp (mind,i) mip.mind_nf_lc
   in
   let irecargs = Array.mapi check_one inds in
   let wfp = Rtree.mk_rec irecargs in
@@ -549,7 +548,7 @@ let check_inductive env kn mib =
   (*  - check constructor types *)
   Array.iter (typecheck_one_inductive env_ar params mib) mib.mind_packets;
   (* check mind_nparams_rec: positivity condition *)
-  check_positivity env_ar params mib.mind_nparams_rec mib.mind_packets;
+  check_positivity env_ar kn params mib.mind_nparams_rec mib.mind_packets;
   (* check mind_equiv... *)
   (* Now we can add the inductive *)
   add_mind kn mib env
diff --git a/checker/indtypes.mli b/checker/indtypes.mli
index bca0a643..4c2b078c 100644
--- a/checker/indtypes.mli
+++ b/checker/indtypes.mli
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: indtypes.mli 9831 2007-05-17 18:55:42Z herbelin $ i*)
-
 (*i*)
 open Names
 open Univ
diff --git a/checker/inductive.ml b/checker/inductive.ml
index b9964fe6..7a04cbfa 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: inductive.ml 10172 2007-10-04 13:02:03Z herbelin $ *)
-
 open Util
 open Names
 open Univ
@@ -83,8 +81,6 @@ let instantiate_params full t args sign =
   if rem_args <> [] then fail();
   substl subs ty
 
-let instantiate_partial_params = instantiate_params false
-
 let full_inductive_instantiate mib params sign =
   let dummy = Prop Null in
   let t = mkArity (sign,dummy) in
@@ -100,10 +96,6 @@ let full_constructor_instantiate ((mind,_),(mib,_),params) =
 
 (* Functions to build standard types related to inductive *)
 
-
-let number_of_inductives mib = Array.length mib.mind_packets
-let number_of_constructors mip = Array.length mip.mind_consnames
-
 (*
 Computing the actual sort of an applied or partially applied inductive type:
 
@@ -346,14 +338,14 @@ let type_case_branches env (ind,largs) (p,pj) c =
 
 
 (************************************************************************)
-(* Checking the case annotation is relevent *)
+(* Checking the case annotation is relevant *)
 
 let check_case_info env indsp ci =
   let (mib,mip) = lookup_mind_specif env indsp in
   if
     not (eq_ind indsp ci.ci_ind) or
     (mib.mind_nparams <> ci.ci_npar) or
-    (mip.mind_consnrealdecls <> ci.ci_cstr_nargs)
+    (mip.mind_consnrealdecls <> ci.ci_cstr_ndecls)
   then raise (TypeError(env,WrongCaseInfo(indsp,ci)))
 
 (************************************************************************)
@@ -404,8 +396,10 @@ type subterm_spec =
   | Dead_code
   | Not_subterm
 
-let spec_of_tree t =
-  if Rtree.eq_rtree (=) t mk_norec then Not_subterm else Subterm(Strict,t)
+let spec_of_tree t = lazy
+  (if Rtree.eq_rtree (=) (Lazy.force t) mk_norec
+   then Not_subterm
+   else Subterm(Strict,Lazy.force t))
 
 let subterm_spec_glb =
   let glb2 s1 s2 =
@@ -440,7 +434,7 @@ let make_renv env minds recarg (kn,tyi) =
     rel_min = recarg+2;
     inds = minds;
     recvec = mind_recvec;
-    genv = [Lazy.lazy_from_val (Subterm(Large,mind_recvec.(tyi)))] }
+    genv = [Lazy.lazy_from_val(Subterm(Large,mind_recvec.(tyi)))] }
 
 let push_var renv (x,ty,spec) =
   { renv with
@@ -459,10 +453,6 @@ let subterm_var p renv =
   try Lazy.force (List.nth renv.genv (p-1))
   with Failure _ | Invalid_argument _ -> Not_subterm
 
-(* Add a variable and mark it as strictly smaller with information [spec]. *)
-let add_subterm renv (x,a,spec) =
-  push_var renv (x,a,lazy (spec_of_tree (Lazy.force spec)))
-
 let push_ctxt_renv renv ctxt =
   let n = rel_context_length ctxt in
   { renv with
@@ -478,6 +468,15 @@ let push_fix_renv renv (_,v,_ as recdef) =
     genv = iterate (fun ge -> Lazy.lazy_from_val Not_subterm::ge) n renv.genv }
 
 
+(* Definition and manipulation of the stack *)
+type stack_element = |SClosure of guard_env*constr |SArg of subterm_spec Lazy.t
+
+let push_stack_closures renv l stack = 
+  List.fold_right (fun h b -> (SClosure (renv,h))::b) l stack
+
+let push_stack_args l stack = 
+  List.fold_right (fun h b -> (SArg h)::b) l stack
+
 (******************************)
 (* Computing the recursive subterms of a term (propagation of size
    information through Cases). *)
@@ -497,60 +496,38 @@ let lookup_subterms env ind =
   let (_,mip) = lookup_mind_specif env ind in
   mip.mind_recargs
 
-(*********************************)
-
-let match_trees t1 t2 =
-  let v1 = dest_subterms t1 in
-  let v2 = dest_subterms t2 in
-  array_for_all2 (fun l1 l2 -> List.length l1 = List.length l2) v1 v2
+let match_inductive ind ra =
+  match ra with
+    | (Mrec i | Imbr i) -> eq_ind ind i
+    | Norec -> false
 
-(* In {match c as z in ind y_s return P with |C_i x_s => t end}
-   [branches_specif renv c_spec ind] returns an array of x_s specs given
-   c_spec the spec of c. *)
-let branches_specif renv c_spec ind =
-  let (_,mip) = lookup_mind_specif renv.env ind in
+(* In {match c as z in ci y_s return P with |C_i x_s => t end}
+   [branches_specif renv c_spec ci] returns an array of x_s specs knowing
+   c_spec. *)
+let branches_specif renv c_spec ci =
   let car = 
     (* We fetch the regular tree associated to the inductive of the match.
        This is just to get the number of constructors (and constructor
        arities) that fit the match branches without forcing c_spec.
        Note that c_spec might be more precise than [v] below, because of
        nested inductive types. *)
+    let (_,mip) = lookup_mind_specif renv.env ci.ci_ind in
     let v = dest_subterms mip.mind_recargs in
       Array.map List.length v in
     Array.mapi
       (fun i nca -> (* i+1-th cstructor has arity nca *)
 	 let lvra = lazy 
 	   (match Lazy.force c_spec with
-		Subterm (_,t) when match_trees mip.mind_recargs t ->
+		Subterm (_,t) when match_inductive ci.ci_ind (dest_recarg t) ->
 		  let vra = Array.of_list (dest_subterms t).(i) in
 		  assert (nca = Array.length vra);
-		  Array.map spec_of_tree vra
+		  Array.map
+		    (fun t -> Lazy.force (spec_of_tree (lazy t)))
+		    vra
 	      | Dead_code -> Array.create nca Dead_code
 	      | _ -> Array.create nca Not_subterm) in
 	 list_tabulate (fun j -> lazy (Lazy.force lvra).(j)) nca)
-      car
-
-(* Propagation of size information through Cases: if the matched
-   object is a recursive subterm then compute the information
-   associated to its own subterms.
-   Rq: if branch is not eta-long, then the recursive information
-   is not propagated to the missing abstractions *)
-let case_branches_specif renv c_spec ind lbr =
-  let vlrec = branches_specif renv c_spec ind in
-  let rec push_branch_args renv lrec c =
-    match lrec with
-        ra::lr ->
-          let c' = whd_betadeltaiota renv.env c in
-          (match c' with
-              Lambda(x,a,b) ->
-                let renv' = push_var renv (x,a,ra) in
-                push_branch_args renv' lr b
-            | _ -> (* branch not in eta-long form: cannot perform rec. calls *)
-                (renv,c'))
-      | [] -> (renv, c) in
-  assert (Array.length vlrec = Array.length lbr);
-  array_map2 (push_branch_args renv) vlrec lbr
- 
+      car 
 
 (* [subterm_specif renv t] computes the recursive structure of [t] and
    compare its size with the size of the initial recursive argument of
@@ -558,78 +535,88 @@ let case_branches_specif renv c_spec ind lbr =
    about variables.
 *)
 
-let rec subterm_specif renv t =
+
+let rec subterm_specif renv stack t =
   (* maybe reduction is not always necessary! *)
   let f,l = decompose_app (whd_betadeltaiota renv.env t) in
-  match f with
-    | Rel k -> subterm_var k renv
-
-    | Case (ci,_,c,lbr) ->
-        let lbr_spec = case_subterm_specif renv ci c lbr in
-        let stl  =
-          Array.map (fun (renv',br') -> subterm_specif renv' br')
-            lbr_spec in
-        subterm_spec_glb stl
-
-    | Fix ((recindxs,i),(_,typarray,bodies as recdef)) ->
-(* when proving that the fixpoint f(x)=e is less than n, it is enough
-   to prove that e is less than n assuming f is less than n
-   furthermore when f is applied to a term which is strictly less than
-   n, one may assume that x itself is strictly less than n
-*)
-        let (ctxt,clfix) = dest_prod renv.env typarray.(i) in
-        let oind =
-          let env' = push_rel_context ctxt renv.env in
-          try Some(fst(find_inductive env' clfix))
-          with Not_found -> None in
-        (match oind with
-            None -> Not_subterm (* happens if fix is polymorphic *)
-          | Some ind ->
-              let nbfix = Array.length typarray in
-              let recargs = lookup_subterms renv.env ind in
-              (* pushing the fixpoints *)
-              let renv' = push_fix_renv renv recdef in
-              let renv' =
-                (* Why Strict here ? To be general, it could also be
-                   Large... *)
-                assign_var_spec renv'
-		  (nbfix-i, Lazy.lazy_from_val (Subterm(Strict,recargs))) in
-              let decrArg = recindxs.(i) in
-              let theBody = bodies.(i)   in
-              let nbOfAbst = decrArg+1 in
-              let sign,strippedBody = decompose_lam_n_assum nbOfAbst theBody in
-              (* pushing the fix parameters *)
-              let renv'' = push_ctxt_renv renv' sign in
-              let renv'' =
-                if List.length l < nbOfAbst then renv''
-                else
-                  let theDecrArg  = List.nth l decrArg in
-	          let arg_spec    = lazy_subterm_specif renv theDecrArg in
-                  assign_var_spec renv'' (1, arg_spec) in
-	      subterm_specif renv'' strippedBody)
-
-    | Lambda (x,a,b) ->
-        assert (l=[]);
-        subterm_specif (push_var_renv renv (x,a)) b
-
-    (* Metas and evars are considered OK *)
-    | (Meta _|Evar _) -> Dead_code
-
-    (* Other terms are not subterms *)
-    | _ -> Not_subterm
-
-and lazy_subterm_specif renv t =
-  lazy (subterm_specif renv t)
-
-and case_subterm_specif renv ci c lbr =
-  if Array.length lbr = 0 then [||]
-  else
-    let c_spec = lazy_subterm_specif renv c in
-    case_branches_specif renv c_spec ci.ci_ind lbr
- 
-(* Check term c can be applied to one of the mutual fixpoints. *)
-let check_is_subterm renv c =
-  match subterm_specif renv c with
+    match f with
+      | Rel k -> subterm_var k renv
+
+      | Case (ci,_,c,lbr) ->
+	  let stack' = push_stack_closures renv l stack in
+          let cases_spec = branches_specif renv 
+	    (lazy_subterm_specif renv [] c) ci in
+          let stl  =
+            Array.mapi (fun i br' ->
+			  let stack_br = push_stack_args (cases_spec.(i)) stack' in
+			    subterm_specif renv stack_br br')
+              lbr in
+            subterm_spec_glb stl
+
+      | Fix ((recindxs,i),(_,typarray,bodies as recdef)) ->
+	  (* when proving that the fixpoint f(x)=e is less than n, it is enough
+	     to prove that e is less than n assuming f is less than n
+	     furthermore when f is applied to a term which is strictly less than
+	     n, one may assume that x itself is strictly less than n
+	  *)
+          let (ctxt,clfix) = dest_prod renv.env typarray.(i) in
+          let oind =
+            let env' = push_rel_context ctxt renv.env in
+              try Some(fst(find_inductive env' clfix))
+              with Not_found -> None in
+            (match oind with
+		 None -> Not_subterm (* happens if fix is polymorphic *)
+               | Some ind ->
+		   let nbfix = Array.length typarray in
+		   let recargs = lookup_subterms renv.env ind in
+		     (* pushing the fixpoints *)
+		   let renv' = push_fix_renv renv recdef in
+		   let renv' =
+                     (* Why Strict here ? To be general, it could also be
+			Large... *)
+                     assign_var_spec renv'
+		       (nbfix-i, lazy (Subterm(Strict,recargs))) in
+		   let decrArg = recindxs.(i) in
+		   let theBody = bodies.(i)   in
+		   let nbOfAbst = decrArg+1 in
+		   let sign,strippedBody = decompose_lam_n_assum nbOfAbst theBody in
+		     (* pushing the fix parameters *)
+		   let stack' = push_stack_closures renv l stack in
+		   let renv'' = push_ctxt_renv renv' sign in
+		   let renv'' =
+                     if List.length stack' < nbOfAbst then renv''
+                     else
+		       let decrArg = List.nth stack' decrArg in
+                       let arg_spec = stack_element_specif decrArg in
+			 assign_var_spec renv'' (1, arg_spec) in
+		     subterm_specif renv'' [] strippedBody)
+
+      | Lambda (x,a,b) ->
+          assert (l=[]);
+	  let spec,stack' = extract_stack renv a stack in
+	    subterm_specif (push_var renv (x,a,spec)) stack' b
+
+      (* Metas and evars are considered OK *)
+      | (Meta _|Evar _) -> Dead_code
+
+      (* Other terms are not subterms *)
+      | _ -> Not_subterm
+
+and lazy_subterm_specif renv stack t =
+  lazy (subterm_specif renv stack t)
+
+and stack_element_specif = function
+  |SClosure (h_renv,h) -> lazy_subterm_specif h_renv [] h
+  |SArg x -> x
+
+and extract_stack renv a = function
+  | [] -> Lazy.lazy_from_val Not_subterm , []
+  | h::t -> stack_element_specif h, t
+
+
+(* Check size x is a correct size for recursive calls. *)
+let check_is_subterm x =
+  match Lazy.force x with
     Subterm (Strict,_) | Dead_code -> true
   |  _ -> false
 
@@ -637,7 +624,7 @@ let check_is_subterm renv c =
 
 exception FixGuardError of env * guard_error
 
-let error_illegal_rec_call renv fx arg =
+let error_illegal_rec_call renv fx (arg_renv,arg) =
   let (_,le_vars,lt_vars) =
     List.fold_left
       (fun (i,le,lt) sbt ->
@@ -647,7 +634,8 @@ let error_illegal_rec_call renv fx arg =
           | _ -> (i+1, le ,lt))
       (1,[],[]) renv.genv in
   raise (FixGuardError (renv.env,
-                        RecursionOnIllegalTerm(fx,arg,le_vars,lt_vars)))
+                        RecursionOnIllegalTerm(fx,(arg_renv.env, arg),
+					       le_vars,lt_vars)))
 
 let error_partial_apply renv fx =
   raise (FixGuardError (renv.env,NotEnoughArgumentsForFixCall fx))
@@ -659,48 +647,57 @@ let check_one_fix renv recpos def =
   let nfi = Array.length recpos in
 
   (* Checks if [t] only make valid recursive calls *)
-  let rec check_rec_call renv t =
+  let rec check_rec_call renv stack t =
     (* if [t] does not make recursive calls, it is guarded: *)
     if noccur_with_meta renv.rel_min nfi t then ()
     else
-      let (f,l) = decompose_app (whd_betaiotazeta renv.env t) in
+      let (f,l) = decompose_app (whd_betaiotazeta t) in
       match f with
         | Rel p ->
             (* Test if [p] is a fixpoint (recursive call) *)
 	    if renv.rel_min <= p & p < renv.rel_min+nfi then
               begin
-                List.iter (check_rec_call renv) l;
+                List.iter (check_rec_call renv []) l;
                 (* the position of the invoked fixpoint: *)
 	        let glob = renv.rel_min+nfi-1-p in
                 (* the decreasing arg of the rec call: *)
 	        let np = recpos.(glob) in
-                if List.length l <= np then error_partial_apply renv glob
+		let stack' = push_stack_closures renv l stack in
+                if List.length stack' <= np then error_partial_apply renv glob
                 else
                   (* Check the decreasing arg is smaller *)
-                  let z = List.nth l np in
-	          if not (check_is_subterm renv z) then
-                    error_illegal_rec_call renv glob z
+                  let z = List.nth stack' np in
+	          if not (check_is_subterm (stack_element_specif z)) then
+                    begin match z with
+		      |SClosure (z,z') -> error_illegal_rec_call renv glob (z,z') 
+		      |SArg _ -> error_partial_apply renv glob
+		    end
               end
             else
               begin
                 match pi2 (lookup_rel p renv.env) with
                 | None ->
-                    List.iter (check_rec_call renv) l
+                    List.iter (check_rec_call renv []) l
                 | Some c ->
-                    try List.iter (check_rec_call renv) l
-                    with FixGuardError _ -> check_rec_call renv (applist(c,l))
+                    try List.iter (check_rec_call renv []) l
+                    with FixGuardError _ ->
+                      check_rec_call renv stack (applist(lift p c,l))
               end
-
+		
         | Case (ci,p,c_0,lrest) ->
-            List.iter (check_rec_call renv) (c_0::p::l);
+            List.iter (check_rec_call renv []) (c_0::p::l);
             (* compute the recarg information for the arguments of
                each branch *)
-            let lbr = case_subterm_specif renv ci c_0 lrest in
-            Array.iter (fun (renv',br') -> check_rec_call renv' br') lbr
+            let case_spec = branches_specif renv 
+	      (lazy_subterm_specif renv [] c_0) ci in
+	    let stack' = push_stack_closures renv l stack in
+              Array.iteri (fun k br' -> 
+			     let stack_br = push_stack_args case_spec.(k) stack' in
+			     check_rec_call renv stack_br br') lrest
 
         (* Enables to traverse Fixpoint definitions in a more intelligent
            way, ie, the rule :
-           if - g = Fix g/p := [y1:T1]...[yp:Tp]e &
+           if - g = fix g (y1:T1)...(yp:Tp) {struct yp} := e &
               - f is guarded with respect to the set of pattern variables S
                 in a1 ... am        &
               - f is guarded with respect to the set of pattern variables S
@@ -710,81 +707,80 @@ let check_one_fix renv recpos def =
                 S+{yp} in e
            then f is guarded with respect to S in (g a1 ... am).
            Eduardo 7/9/98 *)
-
         | Fix ((recindxs,i),(_,typarray,bodies as recdef)) ->
-            List.iter (check_rec_call renv) l;
-            Array.iter (check_rec_call renv) typarray;
+            List.iter (check_rec_call renv []) l;
+            Array.iter (check_rec_call renv []) typarray;
             let decrArg = recindxs.(i) in
             let renv' = push_fix_renv renv recdef in
-            if (List.length l < (decrArg+1)) then
-	      Array.iter (check_rec_call renv') bodies
-            else
+	    let stack' = push_stack_closures renv l stack in
               Array.iteri
                 (fun j body ->
-                  if i=j then
-                    let theDecrArg  = List.nth l decrArg in
-	            let arg_spec = lazy_subterm_specif renv theDecrArg in
-	            check_nested_fix_body renv' (decrArg+1) arg_spec body
-                  else check_rec_call renv' body)
+                   if i=j && (List.length stack' > decrArg) then
+		     let recArg = List.nth stack' decrArg in
+	             let arg_sp = stack_element_specif recArg in
+	             check_nested_fix_body renv' (decrArg+1) arg_sp body
+                   else check_rec_call renv' [] body)
                 bodies
 
         | Const kn ->
             if evaluable_constant kn renv.env then
-              try List.iter (check_rec_call renv) l
+              try List.iter (check_rec_call renv []) l
               with (FixGuardError _ ) ->
-	        check_rec_call renv(applist(constant_value renv.env kn, l))
-	    else List.iter (check_rec_call renv) l
-
-        (* The cases below simply check recursively the condition on the
-           subterms *)
-        | Cast (a,_, b) ->
-            List.iter (check_rec_call renv) (a::b::l)
+		let value = (applist(constant_value renv.env kn, l)) in
+	        check_rec_call renv stack value
+	    else List.iter (check_rec_call renv []) l
 
         | Lambda (x,a,b) ->
-            List.iter (check_rec_call renv) (a::l);
-            check_rec_call (push_var_renv renv (x,a)) b
+	    assert (l = []);
+	    check_rec_call renv [] a ;
+	    let spec, stack' = extract_stack renv a stack in
+	    check_rec_call (push_var renv (x,a,spec)) stack' b
 
         | Prod (x,a,b) ->
-            List.iter (check_rec_call renv) (a::l);
-            check_rec_call (push_var_renv renv (x,a)) b
+	    assert (l = [] && stack = []);
+            check_rec_call renv [] a;
+            check_rec_call (push_var_renv renv (x,a)) [] b
 
         | CoFix (i,(_,typarray,bodies as recdef)) ->
-            List.iter (check_rec_call renv) l;
-	    Array.iter (check_rec_call renv) typarray;
+            List.iter (check_rec_call renv []) l;
+	    Array.iter (check_rec_call renv []) typarray;
 	    let renv' = push_fix_renv renv recdef in
-	    Array.iter (check_rec_call renv') bodies
+	    Array.iter (check_rec_call renv' []) bodies
 
-        | (Ind _ | Construct _ | Sort _) ->
-            List.iter (check_rec_call renv) l
+        | (Ind _ | Construct _) ->
+            List.iter (check_rec_call renv []) l
 
         | Var id ->
             begin
               match pi2 (lookup_named id renv.env) with
               | None ->
-                  List.iter (check_rec_call renv) l
+                  List.iter (check_rec_call renv []) l
               | Some c ->
-                  try List.iter (check_rec_call renv) l
-                  with (FixGuardError _) -> check_rec_call renv (applist(c,l))
+                  try List.iter (check_rec_call renv []) l
+                  with (FixGuardError _) -> 
+		    check_rec_call renv stack (applist(c,l))
             end
 
+	| Sort _ -> assert (l = [])
+
         (* l is not checked because it is considered as the meta's context *)
         | (Evar _ | Meta _) -> ()
 
-        | (App _|LetIn _) -> assert false (* beta zeta reduction *)
+        | (App _ | LetIn _ | Cast _) -> assert false (* beta zeta reduction *)
 
   and check_nested_fix_body renv decr recArgsDecrArg body =
     if decr = 0 then
-      check_rec_call (assign_var_spec renv (1,recArgsDecrArg)) body
+      check_rec_call (assign_var_spec renv (1,recArgsDecrArg)) [] body
     else
       match body with
 	| Lambda (x,a,b) ->
-	    check_rec_call renv a;
+	    check_rec_call renv [] a;
             let renv' = push_var_renv renv (x,a) in
-	    check_nested_fix_body renv' (decr-1) recArgsDecrArg b
+	      check_nested_fix_body renv' (decr-1) recArgsDecrArg b
 	| _ -> anomaly "Not enough abstractions in fix body"
-
+	    
   in
-  check_rec_call renv def
+  check_rec_call renv [] def
 
 
 let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
diff --git a/checker/inductive.mli b/checker/inductive.mli
index e658a798..2cf7c70d 100644
--- a/checker/inductive.mli
+++ b/checker/inductive.mli
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: inductive.mli 9420 2006-12-08 15:34:09Z barras $ i*)
-
 (*i*)
 open Names
 open Term
@@ -80,6 +78,7 @@ type guard_env =
     genv    : subterm_spec Lazy.t list;
   }
 
-val subterm_specif : guard_env -> constr -> subterm_spec
-val case_branches_specif : guard_env -> subterm_spec Lazy.t -> inductive ->
-  constr array -> (guard_env * constr) array
+type stack_element = |SClosure of guard_env*constr |SArg of subterm_spec Lazy.t
+val subterm_specif : guard_env -> stack_element list -> constr -> subterm_spec
+val branches_specif : guard_env -> subterm_spec Lazy.t -> case_info ->
+  subterm_spec Lazy.t list array
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 95387cac..9942816d 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -21,8 +21,8 @@ let refresh_arity ar =
       Sort (Type u) when not (Univ.is_univ_variable u) ->
         let u' = Univ.fresh_local_univ() in
         mkArity (ctxt,Type u'),
-        Univ.enforce_geq u' u Univ.Constraint.empty
-    | _ -> ar, Univ.Constraint.empty
+        Univ.enforce_geq u' u Univ.empty_constraint
+    | _ -> ar, Univ.empty_constraint
 
 let check_constant_declaration env kn cb =
   Flags.if_verbose msgnl (str "  checking cst: " ++ prcon kn);
@@ -33,7 +33,7 @@ let check_constant_declaration env kn cb =
         let ty, cu = refresh_arity ty in
         let envty = add_constraints cu env' in
         let _ = infer_type envty ty in
-        (match cb.const_body with
+        (match body_of_constant cb with
           | Some bd ->
               let j = infer env' (force_constr bd) in
               conv_leq envty j ty
@@ -58,13 +58,6 @@ let rec list_split_assoc k rev_before = function
   | (k',b)::after when k=k' -> rev_before,b,after
   | h::tail -> list_split_assoc k (h::rev_before) tail
 
-let rec list_fold_map2 f e = function
-  |  []  -> (e,[],[])
-  |  h::t ->
-       let e',h1',h2' = f e h in
-       let e'',t1',t2' = list_fold_map2 f e' t in
-	 e'',h1'::t1',h2'::t2'
-
 let check_definition_sub env cb1 cb2 =
   let check_type env t1 t2 =
 
@@ -117,14 +110,19 @@ let check_definition_sub env cb1 cb2 =
   let typ1 = Typeops.type_of_constant_type env cb1.const_type in
   let typ2 = Typeops.type_of_constant_type env cb2.const_type in
   check_type env typ1 typ2;
-  (match cb2 with
-    | {const_body=Some lc2;const_opaque=false} ->
-	let c2 = force_constr lc2 in
-	let c1 = match cb1.const_body with
-	  | Some lc1 -> force_constr lc1
-	  | None -> assert false in
-	Reduction.conv env c1 c2
-    | _ -> ())
+  (* In the spirit of subtyping.check_constant, we accept
+     any implementations of parameters and opaques terms,
+     as long as they have the right type *)
+  (match cb2.const_body with
+    | Undef _ | OpaqueDef _ -> ()
+    | Def lc2 ->
+	(match cb1.const_body with
+	  | Def lc1 ->
+	    let c1 = force_constr lc1 in
+            let c2 = force_constr lc2 in
+	    Reduction.conv env c1 c2
+	  (* Coq only places transparent cb in With_definition_body *)
+	  | _ -> assert false))
 
 let lookup_modtype mp env =
   try Environ.lookup_modtype mp env
@@ -259,14 +257,14 @@ and check_module env mp mb =
 	  {typ_mp=mp;
 	   typ_expr=sign;
 	   typ_expr_alg=None;
-	   typ_constraints=Univ.Constraint.empty;
+	   typ_constraints=Univ.empty_constraint;
 	   typ_delta = mb.mod_delta;}
 	and mtb2 =
 	  {typ_mp=mp;
 	   typ_expr=mb.mod_type;
 	   typ_expr_alg=None;
-	   typ_constraints=Univ.Constraint.empty;
-	   typ_delta = mb.mod_delta;};
+	   typ_constraints=Univ.empty_constraint;
+	   typ_delta = mb.mod_delta;}
 	in
 	let env = add_module (module_body_of_type mp mtb1) env in
 	check_subtypes env mtb1 mtb2
diff --git a/checker/mod_checking.mli b/checker/mod_checking.mli
new file mode 100644
index 00000000..8021ed0f
--- /dev/null
+++ b/checker/mod_checking.mli
@@ -0,0 +1,9 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+val check_module : Environ.env -> Names.module_path -> Declarations.module_body -> unit
diff --git a/checker/modops.ml b/checker/modops.ml
index 38aeaee2..2dc5d062 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: modops.ml 9872 2007-05-30 16:01:18Z soubiran $ i*)
-
 (*i*)
 open Util
 open Pp
@@ -25,8 +23,6 @@ let error_not_a_functor _ = error "Application of not a functor"
 
 let error_incompatible_modtypes _ _ = error "Incompatible module types"
 
-let error_not_equal _ _ = error "Not equal modules"
-
 let error_not_match l _ =
   error ("Signature components for label "^string_of_label l^" do not match")
 
@@ -61,11 +57,6 @@ let destr_functor env mtb =
       	    (arg_id,arg_t,body_t)
   | _ -> error_not_a_functor mtb
 
-
-let is_functor = function
- | SEBfunctor (arg_id,arg_t,body_t) -> true
- | _ -> false
-
 let module_body_of_type mp mtb = 
   { mod_mp = mp;
     mod_type = mtb.typ_expr;
@@ -75,14 +66,6 @@ let module_body_of_type mp mtb =
     mod_delta = mtb.typ_delta;
     mod_retroknowledge = []}
 
-let check_modpath_equiv env mp1 mp2 = 
-  if mp1=mp2 then () else
- (*   let mb1=lookup_module  mp1 env in
-    let mb2=lookup_module mp2 env in
-      if (delta_of_mp mb1.mod_delta mp1)=(delta_of_mp mb2.mod_delta mp2)
-      then ()
-      else*) error_not_equal mp1 mp2
-
 let rec add_signature mp sign resolver env = 
   let add_one env (l,elem) =
     let kn = make_kn mp empty_dirpath l in
@@ -112,23 +95,16 @@ and add_module mb env =
 
 
 let strengthen_const mp_from l cb resolver =
-  match cb.const_opaque, cb.const_body with
-  | false, Some _ -> cb
-  | true, Some _ 
-  | _, None ->
+  match cb.const_body with
+    | Def _ -> cb
+    | _ ->
       let con = make_con mp_from empty_dirpath l in
-     (* let con =  constant_of_delta resolver con in*)
-      let const = Const con in 
-      let const_subs = Some (Declarations.from_val const) in
-	{cb with 
-	   const_body = const_subs;
-	   const_opaque = false;
-	}
-	  
+      (* let con =  constant_of_delta resolver con in*)
+      { cb with const_body = Def (Declarations.from_val (Const con)) }
 
 let rec strengthen_mod mp_from mp_to mb =
   if Declarations.mp_in_delta mb.mod_mp mb.mod_delta then
-    mb 
+    mb
   else
     match mb.mod_type with
      | SEBstruct (sign) -> 
@@ -154,34 +130,33 @@ and strengthen_sig mp_from sign mp_to resolver =
 	resolve_out,item'::rest'
     | (_,SFBmind _ as item):: rest ->
 	let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
-	resolve_out,item::rest'
+	  resolve_out,item::rest'
     | (l,SFBmodule mb) :: rest ->
 	let mp_from' = MPdot (mp_from,l) in
 	let mp_to' = MPdot(mp_to,l) in
 	let mb_out = strengthen_mod mp_from' mp_to' mb in
 	let item' = l,SFBmodule (mb_out) in
 	let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
-	resolve_out, item'::rest'
-    | (l,SFBmodtype mty as item) :: rest ->
+	resolve_out (*add_delta_resolver resolve_out mb.mod_delta*),
+	item':: rest'
+    | (l,SFBmodtype mty as item) :: rest -> 
 	let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
-	resolve_out, item::rest'
+	resolve_out,item::rest'
 
 let strengthen mtb mp =
     match mtb.typ_expr with
-      | SEBstruct (sign) ->
+      | SEBstruct (sign) -> 
 	  let resolve_out,sign_out =
-	    strengthen_sig mtb.typ_mp sign mp mtb.typ_delta
-	  in
-	  {mtb with
-	    typ_expr = SEBstruct(sign_out);
-	    typ_delta = resolve_out(*add_delta_resolver mtb.typ_delta
+	    strengthen_sig mtb.typ_mp sign mp mtb.typ_delta in
+	    {mtb with
+	       typ_expr = SEBstruct(sign_out);
+	       typ_delta = resolve_out(*add_delta_resolver mtb.typ_delta
 		(add_mp_delta_resolver mtb.typ_mp mp resolve_out)*)}
       | SEBfunctor _ -> mtb
       | _ -> anomaly "Modops:the evaluation of the structure failed "
 
 let subst_and_strengthen mb mp =
-  strengthen_mod mb.mod_mp mp
-    (subst_module (map_mp mb.mod_mp mp) mb)
+  strengthen_mod mb.mod_mp mp (subst_module (map_mp mb.mod_mp mp) mb)
 
 
 let module_type_of_module mp mb =
diff --git a/checker/modops.mli b/checker/modops.mli
index 2f9f2e8c..5ed7b0ce 100644
--- a/checker/modops.mli
+++ b/checker/modops.mli
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: modops.mli 9821 2007-05-11 17:00:58Z aspiwack $ i*)
-
 (*i*)
 open Util
 open Names
@@ -33,8 +31,6 @@ val add_signature : module_path -> structure_body -> delta_resolver -> env -> en
 (* adds a module and its components, but not the constraints *)
 val add_module : module_body ->  env -> env
 
-val check_modpath_equiv : env -> module_path -> module_path -> unit
-
 val strengthen : module_type_body -> module_path -> module_type_body
 
 val subst_and_strengthen : module_body -> module_path -> module_body
diff --git a/checker/reduction.ml b/checker/reduction.ml
index ba8ceeef..3aeaa102 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: reduction.ml 9215 2006-10-05 15:40:31Z herbelin $ *)
-
 open Util
 open Names
 open Term
@@ -80,11 +78,11 @@ let pure_stack lfts stk =
 (*                   Reduction Functions                                    *)
 (****************************************************************************)
 
-let whd_betaiotazeta env x =
+let whd_betaiotazeta x =
   match x with
     | (Sort _|Var _|Meta _|Evar _|Const _|Ind _|Construct _|
        Prod _|Lambda _|Fix _|CoFix _) -> x
-    | _ -> whd_val (create_clos_infos betaiotazeta env) (inject x)
+    | _ -> whd_val (create_clos_infos betaiotazeta empty_env) (inject x)
 
 let whd_betadeltaiota env t =
   match t with
@@ -107,15 +105,6 @@ let beta_appvect c v =
       | _ -> applist (substl env t, stack) in
   stacklam [] c (Array.to_list v)
 
-let betazeta_appvect n c v =
-  let rec stacklam n env t stack =
-    if n = 0 then applist (substl env t, stack) else
-    match t, stack with
-        Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl
-      | LetIn(_,b,_,c), _ -> stacklam (n-1) (b::env) c stack
-      | _ -> anomaly "Not enough lambda/let's" in
-  stacklam n [] c (Array.to_list v)
-
 (********************************************************************)
 (*                         Conversion                               *)
 (********************************************************************)
@@ -219,7 +208,7 @@ let rec ccnv univ cv_pb infos lft1 lft2 term1 term2 =
 and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
   Util.check_for_interrupt ();
   (* First head reduce both terms *)
-  let rec  whd_both (t1,stk1) (t2,stk2) =
+  let rec whd_both (t1,stk1) (t2,stk2) =
     let st1' = whd_stack infos t1 stk1 in
     let st2' = whd_stack infos t2 stk2 in
     (* Now, whd_stack on term2 might have modified st1 (due to sharing),
@@ -279,20 +268,10 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
 		    | None -> raise NotConvertible) in
           eqappr univ cv_pb infos app1 app2)
 
-    (* only one constant, defined var or defined rel *)
-    | (FFlex fl1, _)      ->
-        (match unfold_reference infos fl1 with
-           | Some def1 ->
-	       eqappr univ cv_pb infos (lft1, whd_stack infos def1 v1) appr2
-           | None -> raise NotConvertible)
-    | (_, FFlex fl2)      ->
-        (match unfold_reference infos fl2 with
-           | Some def2 ->
-	       eqappr univ cv_pb infos appr1 (lft2, whd_stack infos def2 v2)
-           | None -> raise NotConvertible)
-
     (* other constructors *)
     | (FLambda _, FLambda _) ->
+        (* Inconsistency: we tolerate that v1, v2 contain shift and update but
+           we throw them away *)
         assert (is_empty_stack v1 && is_empty_stack v2);
         let (_,ty1,bd1) = destFLambda mk_clos hd1 in
         let (_,ty2,bd2) = destFLambda mk_clos hd2 in
@@ -305,6 +284,32 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
         ccnv univ CONV infos el1 el2 c1 c'1;
         ccnv univ cv_pb infos (el_lift el1) (el_lift el2) c2 c'2
 
+    (* Eta-expansion on the fly *)
+    | (FLambda _, _) ->
+        if v1 <> [] then
+          anomaly "conversion was given unreduced term (FLambda)";
+        let (_,_ty1,bd1) = destFLambda mk_clos hd1 in
+        eqappr univ CONV infos
+          (el_lift lft1,(bd1,[])) (el_lift lft2,(hd2,eta_expand_stack v2))
+    | (_, FLambda _) ->
+        if v2 <> [] then
+          anomaly "conversion was given unreduced term (FLambda)";
+        let (_,_ty2,bd2) = destFLambda mk_clos hd2 in
+        eqappr univ CONV infos
+          (el_lift lft1,(hd1,eta_expand_stack v1)) (el_lift lft2,(bd2,[]))
+
+    (* only one constant, defined var or defined rel *)
+    | (FFlex fl1, _)      ->
+        (match unfold_reference infos fl1 with
+           | Some def1 ->
+	       eqappr univ cv_pb infos (lft1, whd_stack infos def1 v1) appr2
+           | None -> raise NotConvertible)
+    | (_, FFlex fl2)      ->
+        (match unfold_reference infos fl2 with
+           | Some def2 ->
+	       eqappr univ cv_pb infos appr1 (lft2, whd_stack infos def2 v2)
+           | None -> raise NotConvertible)
+
     (* Inductive types:  MutInd MutConstruct Fix Cofix *)
 
      | (FInd ind1, FInd ind2) ->
@@ -367,37 +372,18 @@ and convert_vect univ infos lft1 lft2 v1 v2 =
 let clos_fconv cv_pb env t1 t2 =
   let infos = create_clos_infos betaiotazeta env in
   let univ = universes env in
-  ccnv univ cv_pb infos ELID ELID (inject t1) (inject t2)
+  ccnv univ cv_pb infos el_id el_id (inject t1) (inject t2)
 
 let fconv cv_pb env t1 t2 =
   if eq_constr t1 t2 then ()
   else clos_fconv cv_pb env t1 t2
 
-let conv_cmp = fconv
 let conv = fconv CONV
 let conv_leq = fconv CUMUL
 
-let conv_leq_vecti env v1 v2 =
-  array_fold_left2_i
-    (fun i _ t1 t2 ->
-      (try conv_leq env t1 t2
-      with (NotConvertible|Invalid_argument _) ->
-        raise (NotConvertibleVect i));
-      ())
-    ()
-    v1
-    v2
-
-(* option for conversion *)
-
-let vm_conv = ref fconv
-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 *)
-      clos_fconv cv_pb env t1 t2
+(* option for conversion : no compilation for the checker *)
+
+let vm_conv = fconv
 
 (********************************************************************)
 (*             Special-Purpose Reduction                            *)
@@ -452,9 +438,3 @@ let dest_arity env c =
     | Sort s -> l,s
     | _ -> error "not an arity"
 
-let is_arity env c =
-  try
-    let _ = dest_arity env c in
-    true
-  with UserError _ -> false
-
diff --git a/checker/reduction.mli b/checker/reduction.mli
index 8e69da44..6695fd03 100644
--- a/checker/reduction.mli
+++ b/checker/reduction.mli
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: reduction.mli 7639 2005-12-02 10:01:15Z gregoire $ i*)
-
 (*i*)
 open Term
 open Environ
@@ -16,7 +14,7 @@ open Environ
 (************************************************************************)
 (*s Reduction functions *)
 
-val whd_betaiotazeta        : env -> constr -> constr
+val whd_betaiotazeta        : constr -> constr
 val whd_betadeltaiota       : env -> constr -> constr
 val whd_betadeltaiota_nolet : env -> constr -> constr
 
@@ -31,7 +29,6 @@ type conv_pb = CONV | CUMUL
 
 val conv           : constr conversion_function
 val conv_leq       : constr conversion_function
-val conv_leq_vecti : constr array conversion_function
 
 val vm_conv : conv_pb -> constr conversion_function
 
@@ -40,9 +37,6 @@ val vm_conv : conv_pb -> constr conversion_function
 (* Builds an application node, reducing beta redexes it may produce. *)
 val beta_appvect : constr -> constr array -> constr
 
-(* Builds an application node, reducing the [n] first beta-zeta redexes. *)
-val betazeta_appvect : int -> constr -> constr array -> constr
-
 (* Pseudo-reduction rule  Prod(x,A,B) a --> B[x\a] *)
 val hnf_prod_applist : env -> constr -> constr list -> constr
 
@@ -54,4 +48,3 @@ val dest_prod       : env -> constr -> rel_context * constr
 val dest_prod_assum : env -> constr -> rel_context * constr
 
 val dest_arity : env -> constr -> arity
-val is_arity   : env -> constr -> bool
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index a669c5e8..bc067dc5 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -1,19 +1,16 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: safe_typing.ml 10275 2007-10-30 11:01:24Z barras $ *)
-
 open Pp
 open Util
 open Names
 open Declarations
 open Environ
-open Mod_checking
 
 (************************************************************************)
 (*
@@ -21,7 +18,6 @@ open Mod_checking
  *)
 
 let genv = ref empty_env
-let reset () = genv := empty_env
 let get_env () = !genv
 
 let set_engagement c =
@@ -63,51 +59,116 @@ let check_imports f caller env needed =
   List.iter check needed
 
 
-
-(* Remove the body of opaque constants in modules *)
-(* also remove mod_expr ? Good idea!*)
-let rec lighten_module mb =
-  { mb with
-    mod_expr = Option.map lighten_modexpr mb.mod_expr;
-    mod_type = lighten_modexpr mb.mod_type }
-
-and lighten_struct struc =
-  let lighten_body (l,body) = (l,match body with
-    | SFBconst ({const_opaque=true} as x) -> SFBconst {x with const_body=None}
-    | (SFBconst _ | SFBmind _ ) as x -> x
-    | SFBmodule m -> SFBmodule (lighten_module m)
-    | SFBmodtype m -> SFBmodtype
-	({m with
-	    typ_expr = lighten_modexpr m.typ_expr}))
-  in
-    List.map lighten_body struc
-
-and lighten_modexpr = function
-  | SEBfunctor (mbid,mty,mexpr) ->
-      SEBfunctor (mbid,
-		    ({mty with
-			typ_expr = lighten_modexpr mty.typ_expr}),
-		  lighten_modexpr mexpr)
-  | SEBident mp as x -> x
-  | SEBstruct ( struc) ->
-      SEBstruct ( lighten_struct struc)
-  | SEBapply (mexpr,marg,u) ->
-      SEBapply (lighten_modexpr mexpr,lighten_modexpr marg,u)
-  | SEBwith (seb,wdcl) ->
-      SEBwith (lighten_modexpr seb,wdcl)
-
-let lighten_library (dp,mb,depends,s) = (dp,lighten_module mb,depends,s)
-
-
 type compiled_library =
     dir_path *
     module_body *
     (dir_path * Digest.t) list *
     engagement option
 
+ (* Store the body of modules' opaque constants inside a table.  
+
+    This module is used during the serialization and deserialization
+    of vo files. 
+
+    By adding an indirection to the opaque constant definitions, we
+    gain the ability not to load them. As these constant definitions
+    are usually big terms, we save a deserialization time as well as
+    some memory space. *)
+module LightenLibrary : sig
+  type table 
+  type lightened_compiled_library 
+  val load : table -> lightened_compiled_library -> compiled_library
+end = struct
+
+  (* The table is implemented as an array of [constr_substituted].
+     Keys are hence integers. To avoid changing the [compiled_library]
+     type, we brutally encode integers into [lazy_constr]. This isn't
+     pretty, but shouldn't be dangerous since the produced structure
+     [lightened_compiled_library] is abstract and only meant for writing
+     to .vo via Marshal (which doesn't care about types).
+  *)
+  type table = constr_substituted array
+  let key_of_lazy_constr (c:lazy_constr) = (Obj.magic c : int)
+
+  (* To avoid any future misuse of the lightened library that could 
+     interpret encoded keys as real [constr_substituted], we hide 
+     these kind of values behind an abstract datatype. *)
+  type lightened_compiled_library = compiled_library
+
+  (* Map a [compiled_library] to another one by just updating 
+     the opaque term [t] to [on_opaque_const_body t]. *)
+  let traverse_library on_opaque_const_body =
+    let rec traverse_module mb =
+      match mb.mod_expr with 
+	  None -> 
+	    { mb with
+		mod_expr = None;
+		mod_type = traverse_modexpr mb.mod_type;
+	    }
+	| Some impl when impl == mb.mod_type-> 
+	    let mtb =  traverse_modexpr mb.mod_type in 
+	      { mb with
+		  mod_expr = Some mtb;
+		  mod_type = mtb;
+	      }    
+	| Some impl -> 
+	    { mb with
+		mod_expr = Option.map traverse_modexpr mb.mod_expr;
+		mod_type = traverse_modexpr mb.mod_type;
+	    }    
+    and traverse_struct struc =
+      let traverse_body (l,body) = (l,match body with
+	| (SFBconst cb) when is_opaque cb ->
+	  SFBconst {cb with const_body = on_opaque_const_body cb.const_body}
+	| (SFBconst _ | SFBmind _ ) as x -> 
+	  x
+	| SFBmodule m -> 
+	  SFBmodule (traverse_module m)
+	| SFBmodtype m -> 
+	  SFBmodtype ({m with typ_expr = traverse_modexpr m.typ_expr}))
+      in
+      List.map traverse_body struc
+	
+    and traverse_modexpr = function
+      | SEBfunctor (mbid,mty,mexpr) ->
+	SEBfunctor (mbid,
+		    ({mty with
+		      typ_expr = traverse_modexpr mty.typ_expr}),
+		    traverse_modexpr mexpr)
+      | SEBident mp as x -> x
+      | SEBstruct (struc) ->
+	SEBstruct  (traverse_struct struc)
+      | SEBapply (mexpr,marg,u) ->
+	SEBapply (traverse_modexpr mexpr,traverse_modexpr marg,u)
+      | SEBwith (seb,wdcl) ->
+	SEBwith (traverse_modexpr seb,wdcl)
+    in
+    fun (dp,mb,depends,s) -> (dp,traverse_module mb,depends,s) 
+
+  (* Loading is also a traversing that decodes the embedded keys that
+     are inside the [lightened_library]. If the [load_proof] flag is
+     set, we lookup inside the table to graft the
+     [constr_substituted]. Otherwise, we set the [const_body] field
+     to [None]. 
+  *)
+  let load table lightened_library =
+    let decode_key = function
+      | Undef _ | Def _ -> assert false
+      | OpaqueDef k ->
+          let k = key_of_lazy_constr k in
+	  let body =
+	    try table.(k)
+	    with _ -> error "Error while retrieving an opaque body"
+	  in
+	  OpaqueDef (lazy_constr_from_val body)
+    in
+    traverse_library decode_key lightened_library
+
+end
+
 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_opt val_eng|]
+let val_deps = val_list (val_tuple ~name:"dep"[|val_dp;no_val|])
+let val_vo = val_tuple ~name:"vo" [|val_dp;val_module;val_deps;val_opt val_eng|]
 
 (* This function should append a certificate to the .vo file.
    The digest must be part of the certicate to rule out attackers
@@ -124,15 +185,15 @@ let import file (dp,mb,depends,engmt as vo) digest =
   let env = !genv in
   check_imports msg_warning dp env depends;
   check_engagement env engmt;
-  check_module (add_constraints mb.mod_constraints env) mb.mod_mp mb;
+  Mod_checking.check_module (add_constraints mb.mod_constraints env) mb.mod_mp mb;
   stamp_library file digest;
   (* We drop proofs once checked *)
 (*  let mb = lighten_module mb in*)
   full_add_module dp mb digest
 
 (* When the module is admitted, digests *must* match *)
-let unsafe_import file (dp,mb,depends,engmt) digest =
-(*  if !Flags.debug then Validate.apply !Flags.debug val_vo vo;*)
+let unsafe_import file (dp,mb,depends,engmt as vo) digest =
+  if !Flags.debug then ignore vo; (*Validate.apply !Flags.debug val_vo vo;*)
   let env = !genv in
   check_imports (errorlabstrm"unsafe_import") dp env depends;
   check_engagement env engmt;
diff --git a/checker/safe_typing.mli b/checker/safe_typing.mli
index 00aa1a84..cd2c06d2 100644
--- a/checker/safe_typing.mli
+++ b/checker/safe_typing.mli
@@ -1,20 +1,17 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: safe_typing.mli 9821 2007-05-11 17:00:58Z aspiwack $ i*)
-
 (*i*)
 open Names
 open Term
 open Environ
 (*i*)
 
-val reset : unit -> unit
 val get_env : unit -> env
 
 (* exporting and importing modules *)
@@ -25,3 +22,19 @@ val import         :
   System.physical_path -> compiled_library -> Digest.t -> unit
 val unsafe_import  :
   System.physical_path -> compiled_library -> Digest.t -> unit
+
+(** Store the body of modules' opaque constants inside a table. 
+
+    This module is used during the serialization and deserialization
+    of vo files. 
+*)
+module LightenLibrary :
+sig
+  type table 
+  type lightened_compiled_library 
+
+  (** [load table lcl] builds a compiled library from a
+      lightened library [lcl] by remplacing every index by its related
+      opaque terms inside [table]. *)
+  val load : table -> lightened_compiled_library -> compiled_library
+end
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 4f113cf9..0c97254b 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: subtyping.ml 10664 2008-03-14 11:27:37Z soubiran $ i*)
-
 (*i*)
 open Util
 open Names
@@ -239,22 +237,29 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
     match info1 with
       | Constant cb1 ->
 	assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ;
-	  (*Start by checking types*)
-	  let cb1 = subst_const_body subst1 cb1 in
-	  let cb2 = subst_const_body subst2 cb2 in
-	  let typ1 = Typeops.type_of_constant_type env cb1.const_type in
-	  let typ2 = Typeops.type_of_constant_type env cb2.const_type in
-	    check_type env typ1 typ2;
-	  let con = make_con mp1 empty_dirpath l in
-	    (match cb2 with
-               | {const_body=Some lc2;const_opaque=false} ->
-		   let c2 = force_constr lc2 in
-		   let c1 = match cb1.const_body with
-		     | Some lc1 -> force_constr lc1
-		     | None -> Const con
-		   in
-		     check_conv conv env c1 c2
-               | _ -> ())
+	let cb1 = subst_const_body subst1 cb1 in
+	let cb2 = subst_const_body subst2 cb2 in
+	(*Start by checking types*)
+	let typ1 = Typeops.type_of_constant_type env cb1.const_type in
+	let typ2 = Typeops.type_of_constant_type env cb2.const_type in
+	check_type env typ1 typ2;
+	(* Now we check the bodies:
+	 - A transparent constant can only be implemented by a compatible
+	   transparent constant.
+         - In the signature, an opaque is handled just as a parameter:
+           anything of the right type can implement it, even if bodies differ.
+	*)
+	(match cb2.const_body with
+	  | Undef _ | OpaqueDef _ -> ()
+	  | Def lc2 ->
+	    (match cb1.const_body with
+	      | Undef _ | OpaqueDef _ -> error ()
+	      | Def lc1 ->
+	        (* NB: cb1 might have been strengthened and appear as transparent.
+	           Anyway [check_conv] will handle that afterwards. *)
+		let c1 = force_constr lc1 in
+		let c2 = force_constr lc2 in
+		check_conv conv env c1 c2))
       | IndType ((kn,i),mind1) ->
 	  ignore (Util.error (
 		    "The kernel does not recognize yet that a parameter can be " ^
@@ -262,7 +267,7 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
 		      "inductive type and give a definition to map the old name to the new " ^
 		      "name."));
       assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ;
-      if cb2.const_body <> None then error () ;
+      if constant_has_body cb2 then error () ;
       let arity1 = type_of_inductive env (mind1,mind1.mind_packets.(i)) in
       let typ2 = Typeops.type_of_constant_type env cb2.const_type in
        check_conv conv_leq env arity1 typ2
@@ -273,7 +278,7 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
        "constructor and give a definition to map the old name to the new " ^
        "name."));
       assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ;
-      if cb2.const_body <> None then error () ;
+      if constant_has_body cb2 then error () ;
       let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in
       let ty2 = Typeops.type_of_constant_type env cb2.const_type in
        check_conv conv env ty1 ty2
@@ -281,7 +286,7 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
 
 let rec check_modules  env msb1 msb2 subst1 subst2 =
   let mty1 = module_type_of_module None msb1 in
-  let mty2 =  module_type_of_module None msb2 in
+  let mty2 = module_type_of_module None msb2 in
     check_modtypes env mty1 mty2 subst1 subst2 false;
  
 
@@ -363,11 +368,5 @@ and check_modtypes  env mtb1 mtb2 subst1 subst2 equiv =
      else check_structure  env mtb1' mtb2' equiv subst1 subst2
 
 let check_subtypes env sup super =
-  (*if sup<>super then*)
   check_modtypes env (strengthen sup sup.typ_mp) super empty_subst
-    (map_mp super.typ_mp sup.typ_mp) false
-
-let check_equal env sup super =
-  (*if sup<>super then*)
-  check_modtypes env sup super empty_subst 
-    (map_mp super.typ_mp sup.typ_mp) true
+      (map_mp super.typ_mp sup.typ_mp) false
diff --git a/checker/subtyping.mli b/checker/subtyping.mli
index d9cbe5ad..ecdf5577 100644
--- a/checker/subtyping.mli
+++ b/checker/subtyping.mli
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: subtyping.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
-
 (*i*)
 open Univ
 open Term
@@ -19,6 +17,5 @@ open Environ
     known by [env] *)
 
 val check_subtypes : env -> module_type_body -> module_type_body -> unit
-val check_equal : env -> module_type_body -> module_type_body -> unit
 
 
diff --git a/checker/term.ml b/checker/term.ml
index 61369586..ab40b6fa 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: term.ml 10098 2007-08-27 11:41:08Z herbelin $ *)
-
 (* This module instantiates the structure of generic deBruijn terms to Coq *)
 
 open Util
@@ -31,15 +29,15 @@ type case_printing =
   { ind_nargs : int; (* length of the arity of the inductive type *)
     style     : case_style }
 type case_info =
-  { ci_ind        : inductive;
-    ci_npar       : int;
-    ci_cstr_nargs : int array; (* number of real args of each constructor *)
-    ci_pp_info    : case_printing (* not interpreted by the kernel *)
+  { ci_ind         : inductive;
+    ci_npar        : int;
+    ci_cstr_ndecls : int array; (* number of pattern var 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|]
+  let val_cprint = val_tuple ~name:"case_printing" [|val_int;val_cstyle|] in
+  val_tuple ~name:"case_info" [|val_ind;val_int;val_array val_int;val_cprint|]
 
 (* Sorts. *)
 
@@ -73,13 +71,14 @@ type 'constr pfixpoint =
 type 'constr pcofixpoint =
     int * 'constr prec_declaration
 
-let val_evar f = val_tuple "pexistential" [|val_int;val_array f|]
+let val_evar f = val_tuple ~name:"pexistential" [|val_int;val_array f|]
 let val_prec f =
-  val_tuple "prec_declaration"[|val_array val_name; val_array f; val_array f|]
+  val_tuple ~name:"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|]
+  val_tuple ~name:"pfixpoint"
+    [|val_tuple~name:"fix2"[|val_array val_int;val_int|];val_prec f|]
+let val_cofix f = val_tuple ~name:"pcofixpoint"[|val_int;val_prec f|]
 
 type cast_kind = VMcast | DEFAULTcast
 let val_cast = val_enum "cast_kind" 2
@@ -262,7 +261,7 @@ let rec exliftn el c = match c with
 (* Lifting the binding depth across k bindings *)
 
 let liftn k n =
-  match el_liftn (pred n) (el_shft k ELID) with
+  match el_liftn (pred n) (el_shft k el_id) with
     | ELID -> (fun c -> c)
     | el -> exliftn el
 
@@ -313,22 +312,15 @@ let subst1 lam = substl [lam]
 (***************************************************************************)
 
 let val_ndecl =
-  val_tuple"named_declaration"[|val_id;val_opt val_constr;val_constr|]
+  val_tuple ~name:"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|]
+  val_tuple ~name:"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
 
-let map_named_declaration f (id, v, ty) = (id, Option.map f v, f ty)
-let map_rel_declaration = map_named_declaration
-
-let fold_named_declaration f (_, v, ty) a = f ty (Option.fold_right f v a)
-let fold_rel_declaration = fold_named_declaration
-
-
 type named_context = named_declaration list
 let empty_named_context = []
 let fold_named_context f l ~init = List.fold_right f l init
@@ -439,7 +431,6 @@ 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 1367e581..0340c79b 100644
--- a/checker/term.mli
+++ b/checker/term.mli
@@ -12,7 +12,7 @@ type case_printing = { ind_nargs : int; style : case_style; }
 type case_info = {
   ci_ind : inductive;
   ci_npar : int;
-  ci_cstr_nargs : int array;
+  ci_cstr_ndecls : int array;
   ci_pp_info : case_printing;
 }
 type contents = Pos | Null
@@ -73,14 +73,6 @@ val subst1 : constr -> constr -> constr
 
 type named_declaration = identifier * constr option * constr
 type rel_declaration = name * constr option * constr
-val map_named_declaration :
-  (constr -> constr) -> named_declaration -> named_declaration
-val map_rel_declaration :
-  (constr -> constr) -> rel_declaration -> rel_declaration
-val fold_named_declaration :
-  (constr -> 'a -> 'a) -> named_declaration -> 'a -> 'a
-val fold_rel_declaration :
-  (constr -> 'a -> 'a) -> rel_declaration -> 'a -> 'a
 type named_context = named_declaration list
 val empty_named_context : named_context
 val fold_named_context :
@@ -111,8 +103,8 @@ 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
+val val_sortfam : Validate.func
+val val_sort : Validate.func
+val val_constr : Validate.func
+val val_rctxt : Validate.func
+val val_nctxt : Validate.func
diff --git a/checker/type_errors.ml b/checker/type_errors.ml
index bd3bb90d..12609832 100644
--- a/checker/type_errors.ml
+++ b/checker/type_errors.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: type_errors.ml 8845 2006-05-23 07:41:58Z herbelin $ *)
-
 open Names
 open Term
 open Environ
@@ -22,7 +20,7 @@ type guard_error =
   (* Fixpoints *)
   | NotEnoughAbstractionInFixBody
   | RecursionNotOnInductiveType of constr
-  | RecursionOnIllegalTerm of int * constr * int list * int list
+  | RecursionOnIllegalTerm of int * (env * constr) * int list * int list
   | NotEnoughArgumentsForFixCall of int
   (* CoFixpoints *)
   | CodomainNotInductiveType of constr
@@ -94,9 +92,6 @@ let error_ill_formed_branch env c i actty expty =
   raise (TypeError (env,
     IllFormedBranch (c,i,nf_betaiota actty, nf_betaiota expty)))
 
-let error_generalization env nvar c =
-  raise (TypeError (env, Generalization (nvar,c)))
-
 let error_actual_type env j expty =
   raise (TypeError (env, ActualType (j,expty)))
 
diff --git a/checker/type_errors.mli b/checker/type_errors.mli
index 82cb3c55..17a210ef 100644
--- a/checker/type_errors.mli
+++ b/checker/type_errors.mli
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: type_errors.mli 8845 2006-05-23 07:41:58Z herbelin $ i*)
-
 (*i*)
 open Names
 open Term
@@ -24,7 +22,7 @@ type guard_error =
   (* Fixpoints *)
   | NotEnoughAbstractionInFixBody
   | RecursionNotOnInductiveType of constr
-  | RecursionOnIllegalTerm of int * constr * int list * int list
+  | RecursionOnIllegalTerm of int * (env * constr) * int list * int list
   | NotEnoughArgumentsForFixCall of int
   (* CoFixpoints *)
   | CodomainNotInductiveType of constr
@@ -86,8 +84,6 @@ val error_number_branches : env -> unsafe_judgment -> int -> 'a
 
 val error_ill_formed_branch : env -> constr -> int -> constr -> constr -> 'a
 
-val error_generalization : env -> name * constr -> unsafe_judgment -> 'a
-
 val error_actual_type : env -> unsafe_judgment -> constr -> 'a
 
 val error_cant_apply_not_functional :
diff --git a/checker/typeops.ml b/checker/typeops.ml
index dffc9fe1..5226db53 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: typeops.ml 9314 2006-10-29 20:11:08Z herbelin $ *)
-
 open Util
 open Names
 open Univ
@@ -91,37 +89,6 @@ let check_args env c hyps =
   with UserError _ | Not_found ->
     error_reference_variables env c
 
-
-(* Checks if the given context of variables [hyps] is included in the
-   current context of [env]. *)
-(*
-let check_hyps id env hyps =
-  let hyps' = named_context env in
-  if not (hyps_inclusion env hyps hyps') then
-    error_reference_variables env id
-*)
-(* Instantiation of terms on real arguments. *)
-
-(* Make a type polymorphic if an arity *)
-
-let extract_level env p =
-  let _,c = dest_prod_assum env p in
-  match c with Sort (Type u) -> Some u | _ -> None
-
-let extract_context_levels env =
-  List.fold_left
-    (fun l (_,b,p) -> if b=None then extract_level env p::l else l) []
-
-let make_polymorphic_if_arity env t =
-  let params, ccl = dest_prod_assum env t in
-  match ccl with
-  | Sort (Type u) ->
-      let param_ccls = extract_context_levels env params in
-      let s = { poly_param_levels = param_ccls; poly_level = u} in
-      PolymorphicArity (params,s)
-  | _ ->
-      NonPolymorphicType t
-
 (* Type of constants *)
 
 let type_of_constant_knowing_parameters env t paramtyps =
@@ -135,9 +102,6 @@ let type_of_constant_knowing_parameters env t paramtyps =
 let type_of_constant_type env t =
   type_of_constant_knowing_parameters env t [||]
 
-let type_of_constant env cst =
-  type_of_constant_type env (constant_type env cst)
-
 let judge_of_constant_knowing_parameters env cst paramstyp =
   let c = Const cst in
   let cb =
@@ -291,7 +255,7 @@ let refresh_arity env ar =
   match hd with
       Sort (Type u) when not (is_univ_variable u) ->
         let u' = fresh_local_univ() in
-        let env' = add_constraints (enforce_geq u' u Constraint.empty) env in
+        let env' = add_constraints (enforce_geq u' u empty_constraint) env in
         env', mkArity (ctxt,Type u')
     | _ -> env, ar
 
@@ -406,12 +370,9 @@ and execute_recdef env (names,lar,vdef) i =
 
 and execute_array env = Array.map (execute env)
 
-and execute_list env = List.map (execute env)
-
 (* Derived functions *)
 let infer env constr = execute env constr
 let infer_type env constr = execute_type env constr
-let infer_v env cv = execute_array env cv
 
 (* Typing of several terms. *)
 
diff --git a/checker/typeops.mli b/checker/typeops.mli
index f4f29fe5..eafe4735 100644
--- a/checker/typeops.mli
+++ b/checker/typeops.mli
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: typeops.mli 9427 2006-12-11 18:46:35Z bgregoir $ i*)
-
 (*i*)
 open Names
 open Term
diff --git a/checker/validate.ml b/checker/validate.ml
index 7d368f05..c5e0bd34 100644
--- a/checker/validate.ml
+++ b/checker/validate.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 (* This module defines validation functions to ensure an imported
    value (using input_value) has the correct structure. *)
 
@@ -38,44 +36,59 @@ let pr_obj o = pr_obj_rec o; Format.print_newline()
 (**************************************************************************)
 (* Obj low-level validators *)
 
-exception ValidObjError of string * Obj.t
-let fail o s = raise (ValidObjError(s,o))
+type error_context = string list
+let mt_ec : error_context = []
+let (/) (ctx:error_context) s : error_context = s::ctx
+let overr (ctx:error_context) f = (fun (_:error_context) -> f ctx) 
+let ext s f (ctx:error_context) = f (ctx/s)
+
 
-let ep s1 f s2 = f (s1^"/"^s2) 
+exception ValidObjError of string * error_context * Obj.t
+let fail ctx o s = raise (ValidObjError(s,ctx,o))
+
+type func = error_context -> Obj.t -> unit
 
 let apply debug f x =
   let o = Obj.repr x in
-  try f o
-  with ValidObjError(msg,obj) ->
+  try f mt_ec o
+  with ValidObjError(msg,ctx,obj) ->
     if debug then begin
       print_endline ("Validation failed: "^msg);
+      print_endline ("Context: "^String.concat"/"(List.rev ctx));
       pr_obj obj
     end;
     failwith "vo structure validation failed"
 
 (* data not validated *)
-let no_val (o:Obj.t) = ()
+let no_val (c:error_context) (o:Obj.t) = ()
 
 (* Check that object o is a block with tag t *)
-let val_tag t o =
+let val_tag t ctx o =
   if Obj.is_block o && Obj.tag o = t then ()
-  else fail o ("expected tag "^string_of_int t)
+  else fail ctx o ("expected tag "^string_of_int t)
 
-let val_block s o =
+let val_block ctx o =
   if Obj.is_block o then
     (if Obj.tag o > Obj.no_scan_tag then
-      fail o (s^": found no scan tag"))
-  else fail o (s^": expected block obj")
+      fail ctx o "block: found no scan tag")
+  else fail ctx o "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 val_tuple ?name v ctx o =
+  let ctx = match name with
+      Some n -> ctx/n
+    | _ -> ctx in
   let n = Array.length v in
-  val_block ("tuple: "^s) o;
-  if Obj.size o = n then Array.iteri (fun i f -> f (Obj.field o i)) v
+  let val_fld i f =
+    f (ctx/("fld="^string_of_int i)) (Obj.field o i) in
+  val_block ctx o;
+  if Obj.size o = n then Array.iteri val_fld v
   else
-    fail o ("tuple:" ^s^" size found:"^string_of_int (Obj.size o))
+    fail ctx o
+      ("tuple size: found "^string_of_int (Obj.size o)^
+	 ", expected "^string_of_int n)
 
 (* Check that the object is either a constant constructor of tag < cc,
    or a constructed variant. each element of vv is an array of
@@ -83,70 +96,79 @@ let val_tuple s v o =
    The size of vv corresponds to the number of non-constant
    constructors, and the size of vv.(i) is the expected arity of the
    i-th non-constant constructor. *)
-let val_sum s cc vv o =
+let val_sum name cc vv ctx o =
+  let ctx = ctx/name in
   if Obj.is_block o then
-    (val_block s o;
+    (val_block (ctx/name) o;
     let n = Array.length vv in
     let i = Obj.tag o in
-    if i < n then val_tuple (s^"(tag "^string_of_int i^")") vv.(i) o
-    else fail o ("bad tag in (sum type) "^s^": found "^string_of_int i))
+    let ctx' = if n=1 then ctx else ctx/("tag="^string_of_int i) in
+    if i < n then val_tuple vv.(i) ctx' o
+    else fail ctx' o ("sum: unexpected tag"))
   else if Obj.is_int o then
     let (n:int) = Obj.magic o in
     (if n<0 || n>=cc then
-      fail o (s^": bad constant constructor "^string_of_int n))
-  else fail o ("not a sum ("^s^")")
+      fail ctx o ("bad constant constructor "^string_of_int n))
+  else fail ctx o "not a sum"
 
 let val_enum s n = val_sum s n [||]
 
 (* Recursive types: avoid looping by eta-expansion *)
-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
+let rec val_rec_sum name cc f ctx o =
+  val_sum name cc (f (overr (ctx/name) (val_rec_sum name cc f))) ctx o
 
 (**************************************************************************)
 (* Builtin types *)
 
 (* Check the o is an array of values satisfying f. *)
-let val_array ?(name="array") f o =
-  val_block name o;
+let val_array ?(pos=false) f ctx o =
+  let upd_ctx =
+    if pos then (fun i -> ctx/string_of_int i) else (fun _ -> ctx) in
+  val_block (ctx/"array") o;
   for i = 0 to Obj.size o - 1 do
-    (f (Obj.field o i):unit)
+    (f (upd_ctx i) (Obj.field o i):unit)
   done
 
 (* Integer validator *)
-let val_int o =
-  if not (Obj.is_int o) then fail o "expected an int"
+let val_int ctx o =
+  if not (Obj.is_int o) then fail ctx o "expected an int"
 
 (* String validator *)
-let val_str o =
-  try val_tag Obj.string_tag o
-  with Failure _ -> fail o "expected a string"
+let val_str ctx o =
+  try val_tag Obj.string_tag ctx o
+  with Failure _ -> fail ctx o "expected a string"
 
 (* Booleans *)
 let val_bool = val_enum "bool" 2
 
 (* Option type *)
-let val_opt ?(name="option") f = val_sum name 1 [|[|f|]|]
+let val_opt ?(name="option") f =
+  val_sum name 1 [|[|f|]|]
 
 (* Lists *)
-let val_list ?(name="list") f =
-  val_rec_sum name 1 (fun vlist -> [|[|f;vlist|]|])
+let val_list ?(name="list") f ctx =
+  val_rec_sum name 1 (fun vlist -> [|[|ext "elem" f;vlist|]|])
+    ctx
 
 (* Reference *)
-let val_ref ?(name="ref") f = val_tuple name [|f|]
+let val_ref ?(name="ref") f ctx =
+  val_tuple [|f|] (ctx/name)
 
 (**************************************************************************)
 (* Standard library types *)
 
 (* Sets *)
 let val_set ?(name="Set.t") f =
-  val_rec_sum name 1 (fun vset -> [|[|vset;f;vset;val_int|]|])
+  val_rec_sum name 1
+    (fun vset -> [|[|vset;ext "elem" f;
+		     vset;ext "bal" val_int|]|])
 
 (* Maps *)
 let rec val_map ?(name="Map.t") fk fv =
-  val_rec_sum name 1 (fun vmap -> [|[|vmap;fk;fv;vmap;val_int|]|])
+  val_rec_sum name 1
+    (fun vmap ->
+       [|[|vmap; ext "key" fk; ext "value" fv;
+	   vmap; ext "bal" val_int|]|])
 
 (**************************************************************************)
 (* Coq types *)
@@ -158,19 +180,19 @@ let val_dp = val_list ~name:"dirpath" val_id
 
 let val_name = val_sum "name" 1 [|[|val_id|]|]
 
-let val_uid = val_tuple "uniq_ident" [|val_int;val_str;val_dp|]
+let val_uid = val_tuple ~name:"uniq_ident" [|val_int;val_str;val_dp|]
 
 let val_mp =
   val_rec_sum "module_path" 0
     (fun vmp -> [|[|val_dp|];[|val_uid|];[|vmp;val_id|]|])
 
-let val_kn = val_tuple "kernel_name" [|val_mp;val_dp;val_id|]
+let val_kn = val_tuple ~name:"kernel_name" [|val_mp;val_dp;val_id|]
 
 let val_con =
-  val_tuple "constant/mutind" [|val_kn;val_kn|]
+  val_tuple ~name:"constant/mutind" [|val_kn;val_kn|]
 
-let val_ind = val_tuple "inductive"[|val_con;val_int|]
-let val_cstr = val_tuple "constructor"[|val_ind;val_int|]
+let val_ind = val_tuple ~name:"inductive"[|val_con;val_int|]
+let val_cstr = val_tuple ~name:"constructor"[|val_ind;val_int|]
 
 (* univ *)
 let val_level = val_sum "level" 1 [|[|val_dp;val_int|]|]
@@ -179,5 +201,5 @@ let val_univ = val_sum "univ" 0
 
 let val_cstrs =
   val_set ~name:"Univ.constraints"
-   (val_tuple "univ_constraint"
+   (val_tuple ~name:"univ_constraint"
      [|val_level;val_enum "order_request" 3;val_level|])