Passage à des contextes de vars et de rels pouvant contenir des déclarations

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

26 files changed, 792 insertions, 662 deletions

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 510e1f12b..e83e1e509 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -19,7 +19,7 @@ type constant_body = {
   const_kind : path_kind;
   const_body : constant_value option;
   const_type : typed_type;
-  const_hyps : typed_type signature;
+  const_hyps : var_context;
   const_constraints : constraints;
   mutable const_opaque : bool }
 
@@ -61,7 +61,7 @@ type one_inductive_body = {
 type mutual_inductive_body = {
   mind_kind : path_kind;
   mind_ntypes : int;
-  mind_hyps : typed_type signature;
+  mind_hyps : var_context;
   mind_packets : one_inductive_body array;
   mind_constraints : constraints;
   mind_singl : constr option;
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 7853a2ce1..1dc4a7cb8 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -20,7 +20,7 @@ type constant_body = {
   const_kind : path_kind;
   const_body : constant_value option;
   const_type : typed_type;
-  const_hyps : typed_type signature;
+  const_hyps : var_context; (* New: younger hyp at top *)
   const_constraints : constraints;
   mutable const_opaque : bool }
 
@@ -66,7 +66,7 @@ type one_inductive_body = {
 type mutual_inductive_body = {
   mind_kind : path_kind;
   mind_ntypes : int;
-  mind_hyps : typed_type signature;
+  mind_hyps : var_context;
   mind_packets : one_inductive_body array;
   mind_constraints : constraints;
   mind_singl : constr option;
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 73a8c6487..217a7f989 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -26,13 +26,21 @@ type globals = {
   env_locals : (global * section_path) list;
   env_imports : import list }
 
+type context = {
+  env_var_context : var_context;
+  env_rel_context : rel_context }
+
 type env = {
   env_context : context;
   env_globals : globals;
   env_universes : universes }
 
+let empty_context = {
+  env_var_context = empty_var_context;
+  env_rel_context = empty_rel_context }
+  
 let empty_env = { 
-  env_context = ENVIRON (nil_sign,nil_dbsign);
+  env_context = empty_context;
   env_globals = {
     env_constants = Spmap.empty;
     env_inductives = Spmap.empty;
@@ -43,29 +51,93 @@ let empty_env = {
 
 let universes env = env.env_universes
 let context env = env.env_context
-let var_context env = let (ENVIRON(g,_)) = env.env_context in g
+let var_context env = env.env_context.env_var_context
+let rel_context env = env.env_context.env_rel_context
 
 (* Construction functions. *)
 
-let push_var idvar env =
-  { env with env_context = add_glob idvar env.env_context }
-
-let change_hyps f env =
-  let (ENVIRON(g,r)) = env.env_context in
-  { env with env_context = ENVIRON (f g, r) }
-
-(* == functions to deal with names in contexts (previously in cases.ml) == *)
-
-(* If cur=(Rel j) then 
- * if env = ENVIRON(sign,[na_h:Th]...[na_j:Tj]...[na_1:T1])
- * then it yields ENVIRON(sign,[na_h:Th]...[Name id:Tj]...[na_1:T1])
- *)
-let change_name_rel env j id = 
-  { env with env_context = change_name_env (context env) j id }
-(****)
-
-let push_rel idrel env =
-  { env with env_context = add_rel idrel env.env_context }
+let map_context f env =
+  let context = env.env_context in
+  { env with
+      env_context = {
+	context with
+	  env_var_context = map_var_context f context.env_var_context ;
+	  env_rel_context = map_rel_context f context.env_rel_context } }
+
+let var_context_app f env =
+  { env with
+      env_context = { env.env_context with
+			env_var_context = f env.env_context.env_var_context } }
+
+let change_hyps = var_context_app
+
+let push_var d   = var_context_app (add_var d)
+let push_var_def def   = var_context_app (add_var_def def)
+let push_var_decl decl = var_context_app (add_var_decl decl)
+let pop_var id         = var_context_app (pop_var id)
+
+let rel_context_app f env =
+  { env with
+      env_context = { env.env_context with
+			env_rel_context = f env.env_context.env_rel_context } }
+
+let reset_context env =
+  { env with
+      env_context = { env_var_context = empty_var_context;
+		      env_rel_context = empty_rel_context} }
+
+let fold_var_context f env a =
+  snd (Sign.fold_var_context
+	 (fun d (env,e) -> (push_var d env, f env d e))
+         (var_context env) (reset_context env,a))
+
+let process_var_context f env =
+  Sign.fold_var_context
+    (fun d env -> f env d) (var_context env) (reset_context env)
+
+let process_var_context_both_sides f env =
+  fold_var_context_both_sides f (var_context env) (reset_context env)
+
+let push_rel d   = rel_context_app (add_rel d)
+let push_rel_def def   = rel_context_app (add_rel_def def)
+let push_rel_decl decl = rel_context_app (add_rel_decl decl)
+let push_rels ctxt     = rel_context_app (concat_rel_context ctxt)
+
+let push_rels_to_vars env =
+  let sign0 = env.env_context.env_var_context in
+  let (subst,_,sign) =
+  List.fold_right
+    (fun (na,c,t) (subst,avoid,sign) ->
+       let na = if na = Anonymous then Name(id_of_string"_") else na in
+       let id = next_name_away na avoid in
+       ((VAR id)::subst,id::avoid,
+	add_var (id,option_app (substl subst) c,typed_app (substl subst) t)
+	  sign))
+    env.env_context.env_rel_context ([],ids_of_var_context sign0,sign0)
+  in subst, (var_context_app (fun _ -> sign) env)
+
+let reset_rel_context env =
+  { env with
+      env_context = { env_var_context = env.env_context.env_var_context;
+		      env_rel_context = empty_rel_context} }
+
+let fold_rel_context f env a =
+  snd (List.fold_right
+	 (fun d (env,e) -> (push_rel d env, f env d e))
+         (rel_context env) (reset_rel_context env,a))
+
+let process_rel_context f env =
+  List.fold_right (fun d env -> f env d)
+    (rel_context env) (reset_rel_context env)
+
+let instantiate_vars = instantiate_sign
+
+let ids_of_context env = 
+  (ids_of_rel_context env.env_context.env_rel_context)
+  @ (ids_of_var_context env.env_context.env_var_context)
+
+let names_of_rel_context env =
+  names_of_rel_context env.env_context.env_rel_context
 
 let set_universes g env =
   if env.env_universes == g then env else { env with env_universes = g }
@@ -109,12 +181,19 @@ let new_meta ()=incr meta_ctr;!meta_ctr;;
 
 (* Access functions. *)
   
-let lookup_var id env =
-  let (_,var) = lookup_glob id env.env_context in
-  (Name id, var)
+let lookup_var_type id env =
+  lookup_id_type id env.env_context.env_var_context
+
+let lookup_var_value id env =
+  lookup_id_value id env.env_context.env_var_context
+
+let lookup_var id env = lookup_id id env.env_context.env_var_context
 
-let lookup_rel n env =
-  Sign.lookup_rel n env.env_context
+let lookup_rel_type n env =
+  Sign.lookup_rel_type n env.env_context.env_rel_context
+
+let lookup_rel_value n env =
+  Sign.lookup_rel_value n env.env_context.env_rel_context
 
 let lookup_constant sp env =
   Spmap.find sp env.env_globals.env_constants
@@ -171,7 +250,7 @@ let hdchar env c =
     | Rel n ->
 	(if n<=k then "p" (* the initial term is flexible product/function *)
 	 else
-	   try match lookup_rel (n-k) env with
+	   try match lookup_rel_type (n-k) env with
 	     | Name id,_ -> lowercase_first_char id
 	     | Anonymous,t -> hdrec 0 (lift (n-k) (body_of_type t))
 	   with Not_found -> "y")
@@ -196,6 +275,32 @@ let it_lambda_name env = List.fold_left (fun c (n,t) ->lambda_name env (n,t,c))
 let prod_create   env (a,b) = mkProd (named_hd env a Anonymous) a b
 let lambda_create env (a,b) =  mkLambda (named_hd env a Anonymous) a b
 
+let name_assumption env (na,c,t) =
+  match c with
+    | None      -> (named_hd env (body_of_type t) na, None, t)
+    | Some body -> (named_hd env body na, c, t)
+
+let prod_assum_name env b d = mkProd_or_LetIn (name_assumption env d) b 
+let lambda_assum_name env b d = mkLambda_or_LetIn (name_assumption env d) b 
+
+let it_mkProd_or_LetIn_name   env = List.fold_left (prod_assum_name env)
+let it_mkLambda_or_LetIn_name env = List.fold_left (lambda_assum_name env)
+
+let it_mkProd_or_LetIn   = List.fold_left (fun c d -> mkProd_or_LetIn d c)
+let it_mkLambda_or_LetIn = List.fold_left (fun c d -> mkLambda_or_LetIn d c)
+
+let it_mkNamedProd_or_LetIn = it_var_context_quantifier mkNamedProd_or_LetIn
+let it_mkNamedLambda_or_LetIn = it_var_context_quantifier mkNamedLambda_or_LetIn
+
+let make_all_name_different env =
+  let avoid = ref (ids_of_var_context (var_context env)) in
+  process_rel_context
+    (fun newenv (na,c,t) -> 
+       let id = next_name_away na !avoid in
+       avoid := id::!avoid;
+       push_rel (Name id,c,t) newenv)
+    env
+
 (* Abstractions. *)
 
 let evaluable_abst env = function
diff --git a/kernel/environ.mli b/kernel/environ.mli
index c8e3642be..616a11162 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -10,26 +10,64 @@ open Univ
 open Sign
 (*i*)
 
-(* Unsafe environments. We define here a datatype for environments. 
+(*s Unsafe environments. We define here a datatype for environments. 
    Since typing is not yet defined, it is not possible to check the
    informations added in environments, and that is what we speak here
    of ``unsafe'' environments. *)
 
+type context
 type env
 
+val empty_context : context
 val empty_env : env
 
 val universes : env -> universes
 val context : env -> context
+val rel_context : env -> rel_context
 val var_context : env -> var_context
 
-val push_var : identifier * typed_type -> env -> env
-val change_hyps : 
-  (typed_type signature -> typed_type signature) -> env -> env
-val change_name_rel : env -> int -> identifier -> env
-
-val push_rel : name * typed_type -> env -> env
-
+(* This forgets var and rel contexts *)
+val reset_context : env -> env
+
+(*s This concerns only the context of local vars referred by names
+    [var_context] *)
+val push_var : var_declaration -> env -> env
+val push_var_decl : identifier * typed_type -> env -> env
+val push_var_def : identifier * constr * typed_type -> env -> env
+val change_hyps : (var_context -> var_context) -> env -> env
+val instantiate_vars : var_context -> constr list -> (identifier * constr) list
+val pop_var : identifier -> env -> env
+
+(*s This concerns only the context of local vars referred by indice
+    [rel_context] *)
+val push_rel : rel_declaration -> env -> env
+val push_rel_decl : name * typed_type -> env -> env
+val push_rel_def : name * constr * typed_type -> env -> env
+val push_rels : rel_context -> env -> env
+val names_of_rel_context : env -> names_context
+
+(*s Returns also the substitution to be applied to rel's *)
+val push_rels_to_vars : env -> constr list * env
+
+(* Gives identifiers in var_context and rel_context *)
+val ids_of_context : env -> identifier list
+val map_context : (constr -> constr) -> env -> env
+
+(*s Recurrence on var_context *)
+val fold_var_context : (env -> var_declaration -> 'a -> 'a) -> env -> 'a -> 'a
+val process_var_context : (env -> var_declaration -> env) -> env -> env
+
+(* [process_var_context_both_sides f env] iters [f] on the var
+   declarations of env taking as argument both the initial segment, the
+   middle value and the tail segment *)
+val process_var_context_both_sides :
+  (env -> var_declaration -> var_context -> env) -> env -> env 
+
+(*s Recurrence on rel_context *)
+val fold_rel_context : (env -> rel_declaration -> 'a -> 'a) -> env -> 'a -> 'a
+val process_rel_context : (env -> rel_declaration -> env) -> env -> env
+
+(*s add entries to environment *)
 val set_universes : universes -> env -> env
 val add_constraints : constraints -> env -> env
 val add_constant : 
@@ -41,13 +79,34 @@ val add_abstraction :
 
 val new_meta : unit -> int
 
-val lookup_var : identifier -> env -> name * typed_type
-val lookup_rel : int -> env -> name * typed_type
+(*s Looks up in environment *)
+
+(* Looks up in the context of local vars referred by names (var_context) *)
+(* raises [Not_found] if the identifier is not found *)
+val lookup_var_type : identifier -> env -> typed_type
+val lookup_var_value : identifier -> env -> constr option
+val lookup_var : identifier -> env -> constr option * typed_type
+
+(* Looks up in the context of local vars referred by indice (rel_context) *)
+(* raises [Not_found] if the index points out of the context *)
+val lookup_rel_type : int -> env -> name * typed_type
+val lookup_rel_value : int -> env -> constr option
+
+(* Looks up in the context of global constant names *)
+(* raises [Not_found] if the required path is not found *)
 val lookup_constant : section_path -> env -> constant_body
+
+(* Looks up in the context of global inductive names *)
+(* raises [Not_found] if the required path is not found *)
 val lookup_mind : section_path -> env -> mutual_inductive_body
 
+(*s Miscellanous *)
 val id_of_global : env -> sorts oper -> identifier
 
+val make_all_name_different : env -> env
+
+(*s Functions creating names for anonymous names *)
+
 val id_of_name_using_hdchar : env -> constr -> name -> identifier
 
 (* [named_hd env t na] just returns [na] is it defined, otherwise it
@@ -68,6 +127,15 @@ val prod_name : env -> name * constr * constr -> constr
 val it_lambda_name : env -> constr -> (name * constr) list -> constr
 val it_prod_name : env -> constr -> (name * constr) list -> constr
 
+val it_mkLambda_or_LetIn_name : env -> constr -> rel_context -> constr
+val it_mkProd_or_LetIn_name : env -> constr -> rel_context -> constr
+
+val it_mkLambda_or_LetIn : constr -> rel_context -> constr
+val it_mkProd_or_LetIn : constr -> rel_context -> constr
+
+val it_mkNamedLambda_or_LetIn : constr -> var_context -> constr
+val it_mkNamedProd_or_LetIn : constr -> var_context -> constr
+
 (* [lambda_create env (t,c)] builds [[x:t]c] where [x] is a name built
    from [t]; [prod_create env (t,c)] builds [(x:t)c] where [x] is a
    name built from [t] *)
diff --git a/kernel/evd.mli b/kernel/evd.mli
index e9f7818ff..3ae00f651 100644
--- a/kernel/evd.mli
+++ b/kernel/evd.mli
@@ -48,6 +48,6 @@ val is_evar : 'a evar_map -> evar -> bool
 
 val is_defined : 'a evar_map -> evar -> bool
 
-val evar_hyps : 'a evar_info -> typed_type signature
+val evar_hyps : 'a evar_info -> var_context
 
 val id_of_existential : evar -> identifier
diff --git a/kernel/generic.ml b/kernel/generic.ml
index 70acca45d..e7e1acc2f 100644
--- a/kernel/generic.ml
+++ b/kernel/generic.ml
@@ -304,10 +304,14 @@ let replace_vars var_alist =
   in 
   if var_alist = [] then (function x -> x) else substrec 0
 
-let subst_varn str n = replace_vars [(str, (Rel n))]
-
 (* (subst_var str t) substitute (VAR str) by (Rel 1) in t *)
-let subst_var str = subst_varn str 1
+let subst_var str = replace_vars [(str, Rel 1)]
+
+(* (subst_vars [id1;...;idn] t) substitute (VAR idj) by (Rel j) in t *)
+let subst_vars vars =
+  let _,subst =
+    List.fold_left (fun (n,l) var -> ((n+1),(var,Rel n)::l)) (1,[]) vars
+  in replace_vars (List.rev subst)
 
 (* [Rel (n+m);...;Rel(n+1)] *)
 
diff --git a/kernel/generic.mli b/kernel/generic.mli
index 3f14efaee..8c2991ff6 100644
--- a/kernel/generic.mli
+++ b/kernel/generic.mli
@@ -60,8 +60,12 @@ val subst1 : 'a term -> 'a term -> 'a term
 val global_vars : 'a term -> identifier list
 
 val global_vars_set : 'a term -> Idset.t
-val subst_var : identifier -> 'a term -> 'a term
 val replace_vars : (identifier * 'a term) list -> 'a term -> 'a term
+val subst_var : identifier -> 'a term -> 'a term
+
+(* [subst_vars [id1;...;idn] t] substitute [VAR idj] by [Rel j] in [t]
+   if two names are identical, the one of least indice is keeped *)
+val subst_vars : identifier list -> 'a term -> 'a term
 
 (* [rel_list n m] and [rel_vect n m] compute [[Rel (n+m);...;Rel(n+1)]] *)
 val rel_vect : int -> int -> 'a term array
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 197f5c299..0536b1f2f 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -27,10 +27,10 @@ open Typeops
 
 type inductive_error =
   (* These are errors related to inductive constructions in this module *)
-  | NonPos of name list * constr * constr
-  | NotEnoughArgs of name list * constr * constr
-  | NotConstructor of name list * constr * constr
-  | NonPar of name list * constr * int * constr * constr
+  | NonPos of env * constr * constr
+  | NotEnoughArgs of env * constr * constr
+  | NotConstructor of env * constr * constr
+  | NonPar of env * constr * int * constr * constr
   | SameNamesTypes of identifier
   | SameNamesConstructors of identifier * identifier
   | NotAnArity of identifier
@@ -74,30 +74,22 @@ let mind_check_names mie =
    for all the given types. *)
 
 let mind_extract_params n c =
-  let (l,c') = decompose_prod_n n c in (List.rev l,c')
+  let (l,c') = decompose_prod_n_assum n c in (l,c')
   
 let extract nparams c =
-  try mind_extract_params nparams c 
+  try fst (mind_extract_params nparams c)
   with UserError _ -> raise (InductiveError BadEntry)
 
-let check_params nparams params c = 
-  let eparams = fst (extract nparams c) in
-  try
-    List.iter2 
-      (fun (n1,t1) (n2,t2) ->
-	 if n1 <> n2 || strip_all_casts t1 <> strip_all_casts t2 then
-	   raise (InductiveError BadEntry))
-      eparams params
-  with Invalid_argument _ ->
-    raise (InductiveError BadEntry)
+let check_params params params' =
+  if not (params = params') then raise (InductiveError BadEntry)
 
 let mind_extract_and_check_params mie =
   let nparams = mie.mind_entry_nparams in
   match mie.mind_entry_inds with
     | [] -> anomaly "empty inductive types declaration"
     | (_,ar,_,_)::l -> 
-	let (params,_) = extract nparams ar in
-	List.iter (fun (_,c,_,_) -> check_params nparams params c) l;
+	let params = extract nparams ar in
+	List.iter (fun (_,c,_,_) -> check_params params (extract nparams c)) l;
 	params
 
 let decomp_all_DLAMV_name constr = 
@@ -110,7 +102,8 @@ let decomp_all_DLAMV_name constr =
 
 let mind_check_lc params mie =
   let nparams = List.length params in
-  let check_lc (_,_,_,lc) = List.iter (check_params nparams params) lc in
+  let check_lc (_,_,_,lc) =
+    List.iter (fun c -> check_params params (extract nparams c)) lc in
   List.iter check_lc mie.mind_entry_inds
 
 let mind_check_arities env mie =
@@ -130,8 +123,6 @@ let allowed_sorts issmall isunit = function
   | Prop Null -> 
       if isunit then [prop;spec] else [prop]
 
-let is_small_type t = is_small t.typ
-
 type ill_formed_ind =
   | LocalNonPos of int
   | LocalNotEnoughArgs of int
@@ -140,9 +131,9 @@ type ill_formed_ind =
 
 exception IllFormedInd of ill_formed_ind
 
-let explain_ind_err ntyp lna nbpar c err = 
+let explain_ind_err ntyp env0 nbpar c err = 
   let (lpar,c') = mind_extract_params nbpar c in
-  let env = (List.map fst lpar)@lna in
+  let env = push_rels lpar env0 in
   match err with
     | LocalNonPos kt -> 
 	raise (InductiveError (NonPos (env,c',Rel (kt+nbpar))))
@@ -290,14 +281,13 @@ let listrec_mconstr env ntypes nparams i indlc =
 	    List.rev lrec
     in check_constr_rec []
   in
-  let lna = it_dbenv (fun l na t -> na::l) [] (context env) in
   Array.map
     (fun c ->
        let c = body_of_type c in
        try
 	 check_construct true (1+nparams) (decomp_par nparams c)
        with IllFormedInd err -> 
-	 explain_ind_err (ntypes-i+1) lna nparams c err)
+	 explain_ind_err (ntypes-i+1) env nparams c err)
     indlc
     
 let is_recursive listind =
@@ -357,7 +347,7 @@ let cci_inductive env env_ar kind nparams finite inds cst =
   let packets = Array.of_list (list_map_i one_packet 1 inds) in
   { mind_kind = kind;
     mind_ntypes = ntypes;
-    mind_hyps = keep_hyps (var_context env) ids;
+    mind_hyps = keep_hyps ids (var_context env);
     mind_packets = packets;
     mind_constraints = cst;
     mind_singl = None;
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 5a7f040d9..46c0255a2 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -15,10 +15,10 @@ open Environ
 
 type inductive_error =
   (* These are errors related to inductive constructions in this module *)
-  | NonPos of name list * constr * constr
-  | NotEnoughArgs of name list * constr * constr
-  | NotConstructor of name list * constr * constr
-  | NonPar of name list * constr * int * constr * constr
+  | NonPos of env * constr * constr
+  | NotEnoughArgs of env * constr * constr
+  | NotConstructor of env * constr * constr
+  | NonPar of env * constr * int * constr * constr
   | SameNamesTypes of identifier
   | SameNamesConstructors of identifier * identifier
   | NotAnArity of identifier
@@ -45,11 +45,11 @@ val mind_check_names : mutual_inductive_entry -> unit
    [mind_entry_inds]. *)
 
 val mind_extract_and_check_params : 
-  mutual_inductive_entry -> (name * constr) list
+  mutual_inductive_entry -> Sign.rel_context
 
-val mind_extract_params : int -> constr -> (name * constr) list * constr
+val mind_extract_params : int -> constr -> Sign.rel_context * constr
 
-val mind_check_lc : (name * constr) list -> mutual_inductive_entry -> unit
+val mind_check_lc : Sign.rel_context -> mutual_inductive_entry -> unit
 
 (* [mind_check_arities] checks that the types declared for all the
    inductive types are some arities. *)
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index cdfd27cd0..43b756651 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -18,6 +18,11 @@ type inductive_instance = {
   mis_args : constr array;
   mis_mip : one_inductive_body }
 
+
+let build_mis ((sp,tyi),args) mib =
+  { mis_sp = sp; mis_mib = mib; mis_tyi = tyi; mis_args = args;
+    mis_mip = mind_nth_type_packet mib tyi }
+
 let mis_ntypes mis = mis.mis_mib.mind_ntypes
 let mis_nparams mis = mis.mis_mib.mind_nparams
 
@@ -36,9 +41,9 @@ let mis_consnames mis = mis.mis_mip.mind_consnames
 let mis_inductive mis = ((mis.mis_sp,mis.mis_tyi),mis.mis_args)
 
 let mis_typed_lc mis =
-  let ids = ids_of_sign mis.mis_mib.mind_hyps in
+  let sign = mis.mis_mib.mind_hyps in
   let args = Array.to_list mis.mis_args in
-  Array.map (fun t -> Instantiate.instantiate_type ids t args)
+  Array.map (fun t -> Instantiate.instantiate_type sign t args)
     mis.mis_mip.mind_nf_lc
 
 let mis_lc mis = Array.map body_of_type (mis_typed_lc mis)
@@ -75,9 +80,9 @@ let mis_type_mconstruct i mispec =
   typed_app (substl (list_tabulate make_Ik ntypes)) specif.(i-1)
 
 let mis_typed_arity mis =
-  let idhyps = ids_of_sign mis.mis_mib.mind_hyps 
+  let hyps = mis.mis_mib.mind_hyps 
   and largs = Array.to_list mis.mis_args in
-  Instantiate.instantiate_type idhyps mis.mis_mip.mind_nf_arity largs
+  Instantiate.instantiate_type hyps mis.mis_mip.mind_nf_arity largs
 
 (*
 let mis_arity mispec = incast_type (mis_typed_arity mispec)
@@ -87,7 +92,7 @@ let mis_arity mis = body_of_type (mis_typed_arity mis)
 
 let mis_params_ctxt mispec =
   let paramsign,_ =
-    decompose_prod_n mispec.mis_mib.mind_nparams
+    decompose_prod_n_assum mispec.mis_mib.mind_nparams
       (body_of_type (mis_typed_arity mispec))
   in paramsign
 
@@ -203,10 +208,8 @@ let find_mcoinductype env sigma c =
     | _ -> raise Induc
 
 (* raise Induc if not an inductive type *)
-let lookup_mind_specif ((sp,tyi),args) env =
-  let mib = lookup_mind sp env in
-  { mis_sp = sp; mis_mib = mib; mis_tyi = tyi; mis_args = args;
-    mis_mip = mind_nth_type_packet mib tyi }
+let lookup_mind_specif ((sp,tyi),args as ind) env =
+  build_mis ind (lookup_mind sp env)
 
 let find_rectype env sigma ty =
   let (mind,largs) = find_mrectype env sigma ty in
@@ -219,7 +222,7 @@ type constructor_summary = {
   cs_cstr : constructor;
   cs_params : constr list;
   cs_nargs : int;
-  cs_args : (name * constr) list;
+  cs_args : rel_context;
   cs_concl_realargs : constr array
 }
 
@@ -227,18 +230,18 @@ let lift_constructor n cs = {
   cs_cstr = (let (csp,ctxt) = cs.cs_cstr in (csp,Array.map (lift n) ctxt));
   cs_params = List.map (lift n) cs.cs_params;
   cs_nargs = cs.cs_nargs;
-  cs_args = lift_context n cs.cs_args;
+  cs_args = lift_rel_context n cs.cs_args;
   cs_concl_realargs = Array.map (liftn n (cs.cs_nargs+1)) cs.cs_concl_realargs
 }
 
 let get_constructor (IndFamily (mispec,params)) j =
   assert (j <= mis_nconstr mispec);
   let typi = mis_type_nf_mconstruct j mispec in
-  let (args,ccl) = decompose_prod (prod_applist typi params) in
+  let (args,ccl) = decompose_prod_assum (prod_applist typi params) in
   let (_,vargs) = array_chop (mis_nparams mispec + 1) (destAppL (ensure_appl ccl)) in
   { cs_cstr = ith_constructor_of_inductive (mis_inductive mispec) j;
     cs_params = params;
-    cs_nargs = List.length args;
+    cs_nargs = rel_context_length args;
     cs_args = args;
     cs_concl_realargs = vargs }
 
@@ -277,8 +280,8 @@ let make_arity env dep indf s =
 let build_branch_type env dep p cs =
   let base = appvect (lift cs.cs_nargs p, cs.cs_concl_realargs) in
   if dep then
-    it_prod_name env
+    it_mkProd_or_LetIn_name env
       (applist (base,[build_dependent_constructor cs]))
       cs.cs_args
   else
-    prod_it base cs.cs_args
+    it_mkProd_or_LetIn base cs.cs_args
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 97118a517..3b45dad0b 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -27,6 +27,8 @@ corresponds various appropriated functions *)
 
 type inductive_instance (* ex-[mind_specif] *)
 
+val build_mis : inductive -> mutual_inductive_body -> inductive_instance
+
 val mis_index : inductive_instance -> int
 val mis_ntypes : inductive_instance -> int
 val mis_nconstr : inductive_instance -> int
@@ -43,7 +45,7 @@ val mis_consnames : inductive_instance -> identifier array
 val mis_typed_arity : inductive_instance -> typed_type
 val mis_inductive : inductive_instance -> inductive
 val mis_arity : inductive_instance -> constr
-val mis_params_ctxt : inductive_instance -> (name * constr) list
+val mis_params_ctxt : inductive_instance -> rel_context
 val mis_sort : inductive_instance -> sorts
 val mis_type_mconstruct : int -> inductive_instance -> typed_type
 
@@ -98,7 +100,7 @@ type constructor_summary = {
   cs_cstr : constructor;
   cs_params : constr list;
   cs_nargs : int;
-  cs_args : (name * constr) list;
+  cs_args : rel_context;
   cs_concl_realargs : constr array
 }
 
@@ -163,6 +165,8 @@ val find_rectype : env -> 'a evar_map -> constr -> inductive_type
 
 val get_constructors : inductive_family -> constructor_summary array
 
+val get_constructor : inductive_family -> int -> constructor_summary
+
 (* [get_arity inf] returns the product and the sort of the
    arity of the inductive family described by [is]; global parameters are
    already instanciated; [indf] must be defined w.r.t. [env] and [sigma];
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index 5ec0e01b0..9fb85961f 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -11,21 +11,22 @@ open Evd
 open Declarations
 open Environ
 
-let is_id_inst ids args =
-  let is_id id = function
-    | VAR id' -> id = id'
+let is_id_inst inst =
+  let is_id = function
+    | id, VAR id' -> id = id'
     | _ -> false
   in
-  List.for_all2 is_id ids args
+  List.for_all is_id inst
 
-let instantiate_constr ids c args =
-  if is_id_inst ids args then
+let instantiate_constr sign c args =
+  let inst = instantiate_vars sign args in
+  if is_id_inst inst then
     c
   else
-    replace_vars (List.combine ids args) c
+    replace_vars inst c
 
-let instantiate_type ids tty args =
-  typed_app (fun c -> instantiate_constr ids c args) tty
+let instantiate_type sign tty args =
+  typed_app (fun c -> instantiate_constr sign c args) tty
 
 (* Constants. *)
 
@@ -33,8 +34,7 @@ let instantiate_type ids tty args =
 let constant_type env sigma (sp,args) =
   let cb = lookup_constant sp env in
   (* TODO: check args *)
-  instantiate_type 
-    (ids_of_sign cb.const_hyps) cb.const_type (Array.to_list args)
+  instantiate_type cb.const_hyps cb.const_type (Array.to_list args)
 
 type const_evaluation_error = NotDefinedConst | OpaqueConst
 
@@ -48,8 +48,7 @@ let constant_value env cst =
   match cb.const_body with
     | Some v -> 
 	let body = cook_constant v in
-        instantiate_constr 
-	  (ids_of_sign cb.const_hyps) body (Array.to_list args)
+        instantiate_constr cb.const_hyps body (Array.to_list args)
     | None ->
 	anomalylabstrm "termenv__constant_value"
 	  [< 'sTR "a defined constant with no body." >]
@@ -62,14 +61,14 @@ let existential_type sigma (n,args) =
   let info = Evd.map sigma n in
   let hyps = evar_hyps info in
   (* TODO: check args [this comment was in Typeops] *)
-  instantiate_constr (ids_of_sign hyps) info.evar_concl (Array.to_list args)
+  instantiate_constr hyps info.evar_concl (Array.to_list args)
 
 let existential_value sigma (n,args) =
   let info = Evd.map sigma n in
   let hyps = evar_hyps info in
   match info.evar_body with
     | Evar_defined c ->
-	instantiate_constr (ids_of_sign hyps) c (Array.to_list args)
+	instantiate_constr hyps c (Array.to_list args)
     | Evar_empty ->
 	anomaly "a defined existential with no body"
 
diff --git a/kernel/instantiate.mli b/kernel/instantiate.mli
index 40601c604..d3454f1cc 100644
--- a/kernel/instantiate.mli
+++ b/kernel/instantiate.mli
@@ -5,15 +5,16 @@
 open Names
 open Term
 open Evd
+open Sign
 open Environ
 (*i*)
 
 (* Instantiation of constants and inductives on their real arguments. *)
 
 val instantiate_constr : 
-  identifier list -> constr -> constr list -> constr
+  var_context -> constr -> constr list -> constr
 val instantiate_type : 
-  identifier list -> typed_type -> constr list -> typed_type
+  var_context -> typed_type -> constr list -> typed_type
 
 type const_evaluation_error = NotDefinedConst | OpaqueConst
 exception NotEvaluableConst of const_evaluation_error
diff --git a/kernel/names.mli b/kernel/names.mli
index 1ccf3c12c..84b25d9cd 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -5,7 +5,7 @@
 open Pp
 (*i*)
 
-(* Names. *)
+(*s Identifiers *)
 
 type identifier
 type name = Name of identifier | Anonymous
@@ -41,6 +41,7 @@ type path_kind = CCI | FW | OBJ
 val string_of_kind : path_kind -> string
 val kind_of_string : string -> path_kind
 
+(*s Section paths *)
 type section_path
 
 val make_path : string list -> identifier -> path_kind -> section_path
@@ -71,6 +72,7 @@ val sp_gt : section_path * section_path -> bool
 module Spset : Set.S with type elt = section_path
 module Spmap : Map.S with type key = section_path
 
+(*s Specific paths for declarations *)
 type inductive_path = section_path * int
 type constructor_path = inductive_path * int
 
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index c7acd792a..c4642b933 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -530,32 +530,27 @@ let contract_fix ((recindices,bodynum),(types,names,bodies as typedbodies)) =
   let make_Fi j = mkFix ((recindices,nbodies-j-1),typedbodies) in
   substl (list_tabulate make_Fi nbodies) bodies.(bodynum)
 
-let fix_recarg fix stack =
-  match fix with 
-    | DOPN(Fix(recindices,bodynum),_) ->
-    	if 0 <= bodynum & bodynum < Array.length recindices then
-	  let recargnum = Array.get recindices bodynum in
-          (try 
-	     Some (recargnum, List.nth stack recargnum)
-           with Failure "nth" | Invalid_argument "List.nth" -> 
-	     None)
-    	else 
-	  None
-    | _ -> assert false
+let fix_recarg ((recindices,bodynum),_) stack =
+  if 0 <= bodynum & bodynum < Array.length recindices then
+    let recargnum = Array.get recindices bodynum in
+    (try 
+       Some (recargnum, List.nth stack recargnum)
+     with Failure "nth" | Invalid_argument "List.nth" -> 
+       None)
+  else 
+    None
 
 let reduce_fix whfun fix stack =
-  match fix with 
-    | DOPN(Fix(recindices,bodynum),bodyvect) ->
-    	(match fix_recarg fix stack with
-           | None -> (false,(fix,stack))
-	   | Some (recargnum,recarg) ->
-               let (recarg'hd,_ as recarg') = whfun recarg [] in
-               let stack' = list_assign stack recargnum (applist recarg') in
-	       (match recarg'hd with
-                  | DOPN(MutConstruct _,_) -> 
-		      (true,(contract_fix (destFix fix),stack'))
-		  | _ -> (false,(fix,stack'))))
-    | _ -> assert false
+  let dfix = destFix fix in
+  match fix_recarg dfix stack with
+    | None -> (false,(fix,stack))
+    | Some (recargnum,recarg) ->
+        let (recarg'hd,_ as recarg') = whfun recarg [] in
+        let stack' = list_assign stack recargnum (applist recarg') in
+	(match recarg'hd with
+           | DOPN(MutConstruct _,_) -> 
+	       (true,(contract_fix dfix,stack'))
+	   | _ -> (false,(fix,stack')))
 
 (* NB : Cette fonction alloue peu c'est l'appel 
      ``let (recarg'hd,_ as recarg') = whfun recarg [] in''
@@ -1035,10 +1030,11 @@ let sort_of_arity env c = snd (splay_arity env Evd.empty c)
 let decomp_n_prod env sigma n = 
   let rec decrec m ln c = if m = 0 then (ln,c) else 
     match whd_betadeltaiota env sigma c with
-      | DOP2(Prod,a,DLAM(n,c_0)) -> decrec (m-1) ((n,a)::ln) c_0
+      | DOP2(Prod,a,DLAM(n,c0)) ->
+	  decrec (m-1) (Sign.add_rel_decl (n,outcast_type a) ln) c0
       | _                      -> error "decomp_n_prod: Not enough products"
   in 
-  decrec n []
+  decrec n Sign.empty_rel_context
 
 
 
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index fb623595a..bab5f446f 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -97,7 +97,7 @@ val splay_prod : env -> 'a evar_map -> constr -> (name * constr) list * constr
 val splay_arity : env -> 'a evar_map -> constr -> (name * constr) list * sorts
 val sort_of_arity : env -> constr -> sorts
 val decomp_n_prod : 
-  env -> 'a evar_map -> int -> constr -> ((name * constr) list) * constr
+  env -> 'a evar_map -> int -> constr -> Sign.rel_context * constr
 
 type 'a miota_args = {
   mP      : constr;     (* the result type *)
@@ -130,7 +130,7 @@ val fold_commands : constr list -> 'a reduction_function
 val pattern_occs : (int list * constr * constr) list -> 'a reduction_function
 val compute : 'a reduction_function
 
-val fix_recarg : constr -> 'a list -> (int * 'a) option
+val fix_recarg : fixpoint -> 'a list -> (int * 'a) option
 val reduce_fix : (constr -> 'a list -> constr * constr list) -> constr ->
   constr list -> bool * (constr * constr list)
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index d4b610a8e..c99bd4bbb 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -48,7 +48,7 @@ let rec execute mf env cstr =
 	(relative env Evd.empty n, cst0)
 
     | IsVar id -> 
-	(make_judge cstr (snd (lookup_var id env)), cst0)
+	(make_judge cstr (lookup_var_type id env), cst0)
 
     | IsAbst _ ->
         if evaluable_abst env cstr then 
@@ -108,7 +108,7 @@ let rec execute mf env cstr =
     | IsLambda (name,c1,c2) -> 
         let (j,cst1) = execute mf env c1 in
         let var = assumption_of_judgment env Evd.empty j in
-	let env1 = push_rel (name,var) env in
+	let env1 = push_rel_decl (name,var) env in
         let (j',cst2) = execute mf env1 c2 in 
         let (j,cst3) = abs_rel env1 Evd.empty name var j' in
 	let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in
@@ -117,7 +117,7 @@ let rec execute mf env cstr =
      | IsProd (name,c1,c2) ->
         let (j,cst1) = execute mf env c1 in
         let varj = type_judgment env Evd.empty j in
-	let env1 = push_rel (name,assumption_of_type_judgment varj) env in
+	let env1 = push_rel_decl (name,assumption_of_type_judgment varj) env in
         let (j',cst2) = execute mf env1 c2 in
 	let (j,cst3) = gen_rel env1 Evd.empty name varj j' in
 	let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in
@@ -137,7 +137,7 @@ and execute_fix mf env lar lfi vdef =
   let nlara = 
     List.combine (List.rev lfi) (Array.to_list (vect_lift_type lara)) in
   let env1 = 
-    List.fold_left (fun env nvar -> push_rel nvar env) env nlara in
+    List.fold_left (fun env nvar -> push_rel_decl nvar env) env nlara in
   let (vdefj,cst2) = execute_array mf env1 vdef in
   let vdefv = Array.map j_val_only vdefj in
   let cst3 = type_fixpoint env1 Evd.empty lfi lara vdefj in
@@ -239,8 +239,9 @@ let universes = universes
 let context = context
 let var_context = var_context
 
+let lookup_var_type = lookup_var_type
+let lookup_rel_type = lookup_rel_type
 let lookup_var = lookup_var
-let lookup_rel = lookup_rel
 let lookup_constant = lookup_constant
 let lookup_mind = lookup_mind
 let lookup_mind_specif = lookup_mind_specif
@@ -248,21 +249,27 @@ let lookup_mind_specif = lookup_mind_specif
 (* Insertion of variables (named and de Bruijn'ed). They are now typed before
    being added to the environment. *)
 
-let push_rel_or_var push (id,c) env =
+let push_rel_or_var_def push (id,c) env =
   let (j,cst) = safe_machine env c in
   let env' = add_constraints cst env in
-  let var = assumption_of_judgment env' Evd.empty j in
-  push (id,var) env'
+  push (id,j.uj_val,j.uj_type) env'
+
+let push_var_def nvar env = push_rel_or_var_def push_var_def nvar env
+
+let push_rel_def nrel env = push_rel_or_var_def push_rel_def nrel env
 
-let push_var nvar env = push_rel_or_var push_var nvar env
+let push_rel_or_var_decl push (id,c) env =
+  let (j,cst) = safe_machine_type env c in
+  let env' = add_constraints cst env in
+  let var = assumption_of_type_judgment j in
+  push (id,var) env'
 
-let push_rel nrel env = push_rel_or_var push_rel nrel env
+let push_var_decl nvar env = push_rel_or_var_decl push_var_decl nvar env
 
-let push_vars vars env =
-  List.fold_left (fun env nvar -> push_var nvar env) env vars
+let push_rel_decl nrel env = push_rel_or_var_decl push_rel_decl nrel env
 
-let push_rels vars env =
-  List.fold_left (fun env nvar -> push_rel nvar env) env vars
+let push_rels_with_univ vars env =
+  List.fold_left (fun env nvar -> push_rel_decl nvar env) env vars
 
 (* Insertion of constants and parameters in environment. *)
 
@@ -291,7 +298,7 @@ let add_constant_with_value sp body typ env =
     const_kind = kind_of_path sp;
     const_body = Some (ref (Cooked body));
     const_type = ty;
-    const_hyps = keep_hyps (var_context env) ids;
+    const_hyps = keep_hyps ids (var_context env);
     const_constraints = Constraint.union cst cst';
     const_opaque = false } 
   in
@@ -305,7 +312,7 @@ let add_lazy_constant sp f t env =
     const_kind = kind_of_path sp;
     const_body = Some (ref (Recipe f));
     const_type = assumption_of_judgment env' Evd.empty jt;
-    const_hyps = keep_hyps (var_context env) ids;
+    const_hyps = keep_hyps ids (var_context env);
     const_constraints = cst;
     const_opaque = false } 
   in
@@ -327,7 +334,7 @@ let add_parameter sp t env =
     const_kind = kind_of_path sp;
     const_body = None;
     const_type = assumption_of_judgment env' Evd.empty jt;
-    const_hyps = keep_hyps (var_context env) ids;
+    const_hyps = keep_hyps ids (var_context env);
     const_constraints = cst;
     const_opaque = false } 
   in
@@ -344,24 +351,21 @@ let max_universe (s1,cst1) (s2,cst2) g =
     | Type u1, _  -> s1, cst1
     | _, _ -> s2, cst2
 
-(* This (re)computes informations relevant to extraction and the sort of
-   an arity or type constructor *)
+(* This (re)computes informations relevant to extraction and the sort of an
+   arity or type constructor; we do not to recompute universes constraints *)
 
 let rec infos_and_sort env t =
   match kind_of_term t with
     | IsProd (name,c1,c2) ->
-        let (varj,cst1) = safe_machine_type env c1 in
+        let (varj,_) = safe_machine_type env c1 in
 	let var = assumption_of_type_judgment varj in
-	let env1 = Environ.push_rel (name,var) env in
-	let (infos,smax,cst) = infos_and_sort env1 c2 in
+	let env1 = Environ.push_rel_decl (name,var) env in
 	let s1 = varj.utj_type in
-	let smax',cst' = max_universe (s1,cst1) (smax,cst) (universes env) in
 	let logic = not (is_info_type env Evd.empty varj) in
 	let small = is_small s1 in
-	((logic,small) :: infos, smax', cst')
+	(logic,small) :: (infos_and_sort env1 c2)
     | IsCast (c,_) -> infos_and_sort env c
-    | _ ->
-	([],prop (* = neutral element of max_universe *),Constraint.empty)
+    | _ -> []
 
 (* [infos] is a sequence of pair [islogic,issmall] for each type in
    the product of a constructor or arity *)
@@ -376,10 +380,12 @@ let is_unit arinfos constrsinfos =
    | [constrinfos] -> is_logic_constr constrinfos && is_logic_arity arinfos
    | _ -> false
 
-let small_unit constrsinfos (env_par,nparams,ar) =
+let small_unit constrsinfos (env_ar,nparams,ar) =
   let issmall = List.for_all is_small constrsinfos in
-  let (arinfos,_,_) =
-    let (_,a) = mind_extract_params nparams ar in infos_and_sort env_par a in
+  let arinfos =
+    let (params,a) = mind_extract_params nparams ar in
+    let env_par = push_rels params env_ar in
+    infos_and_sort env_par a in
   let isunit = is_unit arinfos constrsinfos in
   issmall, isunit
 
@@ -391,14 +397,19 @@ let enforce_type_constructor arsort smax cst =
     | _,_ -> cst
 
 let type_one_constructor env_ar nparams arsort c =
-  let (infos,max,cst1) = 
+  let infos = 
     let (params,dc) = mind_extract_params nparams c in
     let env_par = push_rels params env_ar in
     infos_and_sort env_par dc in
-  let (j,cst2) = safe_machine_type env_ar c in
-  (*C'est idiot, cst1 et cst2 sont essentiellement des copies l'un de l'autre*)
-  let cst3 =enforce_type_constructor arsort max (Constraint.union cst1 cst2) in
-  (infos, assumption_of_type_judgment j, cst3)
+  (* Constructors are typed-checked here *)
+  let (j,cst) = safe_machine_type env_ar c in
+
+  (* If the arity is at some level Type arsort, then the sort of the
+     constructor must be below arsort; here we consider constructors with the
+     global parameters (which add a priori more constraints on their sort) *)
+  let cst2 = enforce_type_constructor arsort j.utj_type cst in
+
+  (infos, assumption_of_type_judgment j, cst2)
 
 let type_one_inductive i env_ar env_par nparams ninds (id,ar,cnames,vc) =
   let arsort = sort_of_arity env_ar ar in
@@ -412,7 +423,7 @@ let type_one_inductive i env_ar env_par nparams ninds (id,ar,cnames,vc) =
   in
   let vc' = Array.of_list jlc in
   let issmall,isunit = small_unit constrsinfos (env_par,nparams,ar) in
-  let (_,tyar) = lookup_rel (ninds+1-i) env_ar in
+  let (_,tyar) = lookup_rel_type (ninds+1-i) env_ar in
   ((id,tyar,cnames,issmall,isunit,vc'), cst)
 
 let add_mind sp mie env =
@@ -425,7 +436,8 @@ let add_mind sp mie env =
   let types_sign = 
     List.map (fun (id,ar,_,_) -> (Name id,ar)) mie.mind_entry_inds
   in
-  let env_arities = push_rels types_sign env in
+  (* Arities with params are typed-checked here *)
+  let env_arities = push_rels_with_univ types_sign env in
   let env_params = push_rels params env_arities in
   let _,inds,cst =
     List.fold_right
@@ -445,18 +457,10 @@ let add_mind sp mie env =
     
 let add_constraints = add_constraints
 
-let pop_vars idl env =
-  let rec remove n sign = 
-    if n = 0 then
-      sign
-    else
-      if isnull_sign sign then anomaly "pop_vars"
-      else
-	let (id,_) = hd_sign sign in 
-	    if not (List.mem id idl) then anomaly "pop_vars";
-	    remove (pred n) (tl_sign sign)
-  in
-  change_hyps (remove (List.length idl)) env
+let rec pop_vars idl env =
+  match idl with 
+    | [] -> env
+    | id::l -> pop_vars l (Environ.pop_var id env)
 
 let export = export
 let import = import
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 5f6b9b073..6d8c80bd0 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -26,8 +26,13 @@ val universes : safe_environment -> universes
 val context : safe_environment -> context
 val var_context : safe_environment -> var_context
 
-val push_var : identifier * constr -> safe_environment -> safe_environment
-val push_rel : name * constr -> safe_environment -> safe_environment
+val push_var_decl : identifier * constr -> safe_environment -> safe_environment
+val push_var_def : identifier * constr -> safe_environment -> safe_environment
+(*
+val push_rel_decl : name * constr -> safe_environment -> safe_environment
+val push_rel_def : name * constr -> safe_environment -> safe_environment
+*)
+
 val add_constant : 
   section_path -> constant_entry -> safe_environment -> safe_environment
 val add_lazy_constant : 
@@ -42,8 +47,10 @@ val add_constraints : constraints -> safe_environment -> safe_environment
 
 val pop_vars : identifier list -> safe_environment -> safe_environment
 
-val lookup_var : identifier -> safe_environment -> name * typed_type
+val lookup_var : identifier -> safe_environment -> constr option * typed_type
+(*
 val lookup_rel : int -> safe_environment -> name * typed_type
+*)
 val lookup_constant : section_path -> safe_environment -> constant_body
 val lookup_mind : section_path -> safe_environment -> mutual_inductive_body
 val lookup_mind_specif : inductive -> safe_environment -> inductive_instance
diff --git a/kernel/sign.ml b/kernel/sign.ml
index fb2c8d31d..edee43885 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -8,251 +8,190 @@ open Term
 
 (* Signatures *)
 
-type 'a signature = identifier list * 'a list
-type 'a db_signature = (name * 'a) list
-type ('a,'b) sign = ENVIRON of 'a signature * 'b db_signature
-
-let gLOB hyps = ENVIRON (hyps,[])
-
-let ids_of_sign (idl,_) = idl
-let vals_of_sign (_,vals) = vals
-let add_sign (id,ty) (idl,tyl) = (id::idl,ty::tyl)
-let sign_it f (idl,tyl) e = List.fold_right2 f idl tyl e
-let it_sign f e (idl,tyl) = List.fold_left2 f e idl tyl
-let nil_sign = ([],[])
-let rev_sign (idl,tyl) = (List.rev idl, List.rev tyl)
-let map_sign_typ f (idl,tyl) = (idl, List.map f tyl)
-let concat_sign (idl1,tyl1) (idl2,tyl2) = (idl1@idl2, tyl1@tyl2)
-let diff_sign (idl1,tyl1) (idl2,tyl2) = 
-  (list_subtract idl1 idl2, list_subtract tyl1 tyl2)
-let nth_sign (idl,tyl) n = (List.nth idl (n-1), List.nth tyl (n-1))
-let map_sign_graph f (ids,tys) = List.map2 f ids tys
-
-let isnull_sign = function 
-  | ([],[])     -> true
-  | (_::_,_::_) -> false
-  | _           -> invalid_arg "isnull_sign"
-
-let hd_sign = function
-  | (id::_,ty::_) -> (id,ty)
-  | _             -> failwith "hd_sign"
-
-let tl_sign = function
-  | (_::idl,_::tyl) -> (idl,tyl)
-  | _               -> failwith "tl_sign"
-
-let lookup_sign id (dom,rang) = 
-  let rec aux = function
-    | ([],          [])        -> raise Not_found
-    | ((id'::id'l), (ty::tyl)) -> if id' = id then (id',ty) else aux (id'l,tyl)
-    | _                        -> anomaly "Names: lookup_sign"
+let add d sign = d::sign
+let map f = List.map (fun (na,c,t) -> (na,option_app f c,typed_app f t))
+
+let add_decl (n,t) sign = (n,None,t)::sign
+let add_def (n,c,t) sign = (n,Some c,t)::sign
+
+type var_declaration = identifier * constr option * typed_type
+type var_context = var_declaration list
+
+let add_var = add
+let add_var_decl = add_decl
+let add_var_def = add_def
+let rec lookup_id_type id = function
+  | (id',c,t) :: _ when id=id' -> t
+  | _ :: sign -> lookup_id_type id sign
+  | [] -> raise Not_found
+let rec lookup_id_value id = function
+  | (id',c,t) :: _ when id=id' -> c
+  | _ :: sign -> lookup_id_value id sign
+  | [] -> raise Not_found
+let rec lookup_id id = function
+  | (id',c,t) :: _ when id=id' -> (c,t)
+  | _ :: sign -> lookup_id id sign
+  | [] -> raise Not_found
+let empty_var_context = []
+let pop_var id = function
+  | (id',_,_) :: sign -> assert (id = id'); sign
+  | [] -> assert false
+let ids_of_var_context = List.map (fun (id,_,_) -> id)
+let map_var_context = map
+let rec mem_var_context id = function
+  | (id',_,_) :: _ when id=id' -> true
+  | _ :: sign -> mem_var_context id sign
+  | [] -> false
+let fold_var_context = List.fold_right
+let fold_var_context_both_sides = list_fold_right_and_left
+let it_var_context_quantifier f = List.fold_left (fun c d -> f d c)
+
+type rel_declaration = name * constr option * typed_type
+type rel_context = rel_declaration list
+
+let add_rel = add
+let add_rel_decl = add_decl
+let add_rel_def = add_def
+let lookup_rel_type n sign =
+  let rec lookrec = function
+    | (1, (na,_,t) :: _) -> (na,t)
+    | (n, _ :: sign)     -> lookrec (n-1,sign)
+    | (_, [])            -> raise Not_found
   in 
-  aux (dom,rang)
-
-let list_of_sign (ids,tys) =
-  try List.combine ids tys
-  with _ -> anomaly "Corrupted signature"
-
-
-let make_sign = List.split
-let do_sign f (ids,tys) = List.iter2 f ids tys
-
-let uncons_sign = function
-  | (id::idl,ty::tyl) -> ((id,ty),(idl,tyl))
-  | _ -> anomaly "signatures are being manipulated in a non-abstract way"
-
-let sign_length (idl,tyl) =
-  let lenid = List.length idl
-  and lenty = List.length tyl in
-  if lenid = lenty then 
-    lenid
-  else 
-    invalid_arg "lookup_sign"
-
-let mem_sign sign id = List.mem id (ids_of_sign sign)
-
-let modify_sign id ty = 
-  let rec modrec = function
-    | [],[] -> invalid_arg "modify_sign"
-    | sign  -> 
-	let (id',ty') = hd_sign sign in
-	if id = id' then
-      	  add_sign (id,ty) (tl_sign sign)
-	else
-      	  add_sign (id',ty') (modrec (tl_sign sign))
+  lookrec (n,sign)
+let lookup_rel_value n sign =
+  let rec lookrec = function
+    | (1, (_,c,_) :: _) -> c
+    | (n, _ :: sign )   -> lookrec (n-1,sign)
+    | (_, [])           -> raise Not_found
   in 
-  modrec
-
-let exists_sign f = 
-  let rec exrec sign =
-    if isnull_sign sign then 
-      false
-    else 
-      let ((id,t),tl) = uncons_sign sign in
-      f id t or exrec tl
+  lookrec (n,sign)
+let rec lookup_rel_id id sign = 
+  let rec lookrec = function
+    | (n, (Anonymous,_,_)::l) -> lookrec (n+1,l)
+    | (n, (Name id',_,t)::l)  -> if id' = id then (n,t) else lookrec (n+1,l)
+    | (_, [])                 -> raise Not_found
   in 
-  exrec
-
-(* [sign_prefix id sign] returns the signature up to and including id,
-   with all later assumptions stripped off.  It is an error to call it
-   with a signature not containing id, and that error is generated
-   with error. *)
-
-let sign_prefix id sign = 
-  let rec prefrec sign =
-    if isnull_sign sign then
-      error "sign_prefix"
-    else
-      let ((id',t),sign') = uncons_sign sign in
-      if id' = id then sign else prefrec sign'
+  lookrec (1,sign)
+let empty_rel_context = []
+let rel_context_length = List.length
+let lift_rel_context n sign =
+  let rec liftrec k = function
+    | (na,c,t)::sign ->
+	(na,option_app (liftn n k) c,typed_app (liftn n k) t)
+	::(liftrec (k-1) sign)
+    | [] -> []
+  in
+  liftrec (rel_context_length sign) sign
+let concat_rel_context = (@)
+let ids_of_rel_context sign =
+  List.fold_right
+    (fun (na,_,_) l -> match na with Name id -> id::l | Anonymous -> l)
+    sign []
+let names_of_rel_context = List.map (fun (na,_,_) -> na)
+let decls_of_rel_context sign =
+  List.fold_right
+    (fun (na,c,t) l -> match c with Some _ -> l | None -> (na,body_of_type t)::l)
+    sign []
+let map_rel_context = map
+
+let instantiate_sign sign args =
+  let rec instrec = function
+    | ((id,None,_) :: sign, c::args) -> (id,c) :: (instrec (sign,args))
+    | ((id,Some c,_) :: _, args)     -> (id,c) :: (instrec (sign,args))
+    | ([],[])                       -> []
+    | ([],_) | (_,[]) ->
+    anomaly "Signature and its instance do not match"
   in 
-  prefrec sign
-
-let add_sign_after whereid (id,t) sign = 
-  let rec addrec sign =
-    if isnull_sign sign then
-      error "add_sign_after"
-    else
-      let ((id',t'),sign') = uncons_sign sign in
-      if id' = whereid then add_sign (id,t) sign
-      else add_sign (id',t') (addrec sign')
+  instrec (sign,args)
+
+(* [keep_hyps sign ids] keeps the part of the signature [sign] which 
+   contains the variables of the set [ids], and recursively the variables 
+   contained in the types of the needed variables. *)
+
+let rec keep_hyps needed = function
+  | (id,copt,t as d) ::sign when Idset.mem id needed ->
+      let globc = 
+	match copt with
+	  | None -> Idset.empty
+	  | Some c -> global_vars_set c in
+      let needed' =
+	Idset.union (global_vars_set (body_of_type t)) 
+	  (Idset.union globc needed) in
+      d :: (keep_hyps needed' sign)
+  | _::sign -> keep_hyps needed sign
+  | [] -> []
+
+(*************************)
+(*   Names environments  *)
+(*************************)
+type names_context = name list
+let add_name n nl = n::nl
+let lookup_name_of_rel p names =
+  try List.nth names (p-1)
+  with Failure "nth" -> raise Not_found
+let rec lookup_rel_of_name id names = 
+  let rec lookrec n = function
+    | Anonymous :: l  -> lookrec (n+1) l
+    | (Name id') :: l -> if id' = id then n else lookrec (n+1) l
+    | []            -> raise Not_found
   in 
-  addrec sign
-
-let add_sign_replacing whereid (id,t) sign = 
-  let rec addrec sign =
-    if isnull_sign sign then
-      error "add_replacing_after"
-    else
-      let ((id',t'),sign') = uncons_sign sign in
-      if id' = whereid then add_sign (id,t) sign'
-      else add_sign (id',t') (addrec sign')
+  lookrec 1 names
+let empty_names_context = []
+
+(*********************************)
+(*       Term destructors        *)
+(*********************************)
+
+(* Transforms a product term (x1:T1)..(xn:Tn)T into the pair
+   ([(xn,Tn);...;(x1,T1)],T), where T is not a product *)
+let decompose_prod_assum = 
+  let rec prodec_rec l = function
+    | DOP2(Prod,t,DLAM(x,c)) ->
+	prodec_rec (add_rel_decl (x,outcast_type t) l) c
+(*    | Letin,t,DLAM(x,c)) ->
+	prodec_rec (add_rel_def (x,c,outcast_type t) l) c*)
+    | DOP2(Cast,c,_)         -> prodec_rec l c
+    | c                      -> l,c
   in 
-  addrec sign
-  
-(* [prepend_sign Gamma1 Gamma2]
-   prepends Gamma1 to the front of Gamma2, given that their namespaces
-   are distinct. *)
-
-let prepend_sign gamma1 gamma2 =
-  if [] = list_intersect (ids_of_sign gamma1) (ids_of_sign gamma2) then
-    let (ids1,vals1) = gamma1
-    and (ids2,vals2) = gamma2 in
-    (ids1@ids2, vals1@vals2)
-  else
-    invalid_arg "prepend_sign"
-
-let dunbind default sign ty = function 
-  | DLAM(na,c) ->
-      let id = next_ident_away (id_of_name default na) (ids_of_sign sign) in
-      (add_sign (id,ty) sign, subst1 (VAR id) c)
-  | _ -> invalid_arg "dunbind default"
-
-let dunbindv default sign ty = function
-  | DLAMV(na,c) ->
-      let id = next_ident_away (id_of_name default na) (ids_of_sign sign) in 
-      (add_sign (id,ty) sign,Array.map (subst1 (VAR id)) c)
-  | _ -> invalid_arg "dunbindv default"
-
-let dbind sign c =
-  let (id,ty) = hd_sign sign
-  and sign' = tl_sign sign in
-  (ty,DLAM(Name id,subst_var id c))
-
-let dbindv sign cl =
-  let (id,ty) = hd_sign sign
-  and sign' = tl_sign sign in
-  (ty,DLAMV(Name id,Array.map (subst_var id) cl))
-
-(* de Bruijn environments *)
-
-let nil_dbsign = []
-
-(* Signatures + de Bruijn environments *)
-
-let dbenv_it f (ENVIRON(_,dbs)) init =
-  List.fold_right (fun (na,t) v -> f na t v) dbs init
-
-let it_dbenv f init (ENVIRON(_,dbs)) =
-  List.fold_left (fun v (na,t) -> f v na t) init dbs
-
-let isnull_rel_env (ENVIRON(_,dbs)) = (dbs = [])
-let uncons_rel_env (ENVIRON(sign,dbs)) = List.hd dbs,ENVIRON(sign,List.tl dbs)
-
-let ids_of_env (ENVIRON(sign,dbenv)) =
-  let filter (n,_) l = match n with (Name id) -> id::l | Anonymous -> l in
-  (ids_of_sign sign) @ (List.fold_right filter dbenv [])
-
-let get_globals (ENVIRON(g,_)) = g
-let get_rels (ENVIRON(_,r)) = r
-
-let add_rel (n,x) (ENVIRON(g,r)) = (ENVIRON(g,(n,x)::r))
-
-let add_glob (id,x) (ENVIRON((dom,rang),r)) = (ENVIRON((id::dom,x::rang),r))
-
-let lookup_glob id (ENVIRON((dom,rang),_)) = 
-  let rec aux = function
-    | ([],          [])        -> raise Not_found
-    | ((id'::id'l), (ty::tyl)) -> if id' = id then (id',ty) else aux (id'l,tyl)
-    | _                        -> anomaly "Names: lookup_glob"
+  prodec_rec empty_rel_context
+
+(* Transforms a lambda term [x1:T1]..[xn:Tn]T into the pair
+   ([(xn,Tn);...;(x1,T1)],T), where T is not a lambda *)
+let decompose_lam_assum = 
+  let rec lamdec_rec l = function
+    | DOP2(Lambda,t,DLAM(x,c)) ->
+	lamdec_rec (add_rel_decl (x,outcast_type t) l) c
+(*    | Letin,t,DLAM(x,c)) ->
+	lamdec_rec (add_rel_def (x,c,outcast_type t) l) c*)
+    | DOP2(Cast,c,_)         -> lamdec_rec l c
+    | c                      -> l,c
   in 
-  aux (dom,rang)
-
-let mem_glob id (ENVIRON((dom,_),_)) = List.mem id dom
-
-let lookup_rel n (ENVIRON(_,r)) = 
-  let rec lookrec n l = match (n,l) with
-    | (1, ((na,x)::l)) -> (na,x)
-    | (n, (_::l))      -> lookrec (n-1) l
-    | (_, [])          -> raise Not_found
+  lamdec_rec empty_rel_context
+
+(* Given a positive integer n, transforms a product term (x1:T1)..(xn:Tn)T 
+   into the pair ([(xn,Tn);...;(x1,T1)],T) *)
+let decompose_prod_n_assum n =
+  if n < 0 then error "decompose_prod_n: integer parameter must be positive";
+  let rec prodec_rec l n c = 
+    if n=0 then l,c 
+    else match c with 
+      | DOP2(Prod,t,DLAM(x,c)) -> prodec_rec (add_rel_decl (x,outcast_type t) l) (n-1) c
+      | DOP2(Cast,c,_)         -> prodec_rec l n c
+      | c -> error "decompose_prod_n: not enough products"
   in 
-  lookrec n r
-
-let rec lookup_rel_id id (ENVIRON(_,r)) = 
-  let rec lookrec = function
-    | (n, ((Anonymous,x)::l)) -> lookrec (n+1,l)
-    | (n, ((Name id',x)::l))  -> if id' = id then (n,x) else lookrec (n+1,l)
-    | (_, [])                 -> raise Not_found
+  prodec_rec empty_rel_context n 
+
+(* Given a positive integer n, transforms a lambda term [x1:T1]..[xn:Tn]T 
+   into the pair ([(xn,Tn);...;(x1,T1)],T) *)
+let decompose_lam_n_assum n =
+  if n < 0 then error "decompose_lam_n: integer parameter must be positive";
+  let rec lamdec_rec l n c = 
+    if n=0 then l,c 
+    else match c with 
+      | DOP2(Lambda,t,DLAM(x,c)) -> lamdec_rec (add_rel_decl (x,outcast_type t) l) (n-1) c
+      | DOP2(Cast,c,_)           -> lamdec_rec l n c
+      | c -> error "decompose_lam_n: not enough abstractions"
   in 
-  lookrec (1,r)
-
-let map_rel_env f (ENVIRON(g,r)) =
-  ENVIRON (g,List.map (fun (na,x) -> (na,f x)) r)
-
-let map_var_env f (ENVIRON((dom,rang),r)) =
-  ENVIRON (List.fold_right2 
-	     (fun na x (doml,rangl) -> (na::doml,(f x)::rangl))
-      	     dom rang ([],[]),r)
-
-let number_of_rels (ENVIRON(_,db)) = List.length db
-
-let change_name_env (ENVIRON(sign,db)) j id =
-  match list_chop (j-1) db with
-    | db1,((_,ty)::db2) -> ENVIRON(sign,db1@(Name id,ty)::db2)
-    | _ -> raise Not_found
-
-let unitize_env env = map_rel_env (fun _ -> ()) env
-
-type ('b,'a) search_result =
-  | GLOBNAME of identifier  * 'b
-  | RELNAME of int * 'a
-
-let lookup_id id env =
-  try 
-    let (x,y) = lookup_rel_id id env in RELNAME(x,y)
-  with 
-    | Not_found -> let (x,y) = lookup_glob id env in GLOBNAME(x,y)
-
-let make_all_name_different (ENVIRON((dom,_) as sign,dbs)) =
-  let _,newdbs =
-    List.fold_right
-      (fun (na,t) (avoid,newdbs) -> 
-	 let id = next_name_away na avoid in
-	 (id::avoid),((Name id,t)::newdbs))
-      dbs (dom,[])
-  in ENVIRON (sign,newdbs)
-
-type 'b assumptions = (typed_type,'b) sign
-type context = (typed_type,typed_type) sign
-type var_context = typed_type signature
+  lamdec_rec empty_rel_context n 
 
diff --git a/kernel/sign.mli b/kernel/sign.mli
index 763a67471..3add55894 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -7,107 +7,75 @@ open Generic
 open Term
 (*i*)
 
-(* Signatures of named variables. *)
-
-type 'a signature
-
-val nil_sign : 'a signature
-val add_sign : (identifier * 'a) -> 'a signature -> 'a signature
-val lookup_sign : identifier -> 'a signature -> (identifier * 'a)
-
-val rev_sign : 'a signature -> 'a signature
-val map_sign_typ : ('a -> 'b) -> 'a signature -> 'b signature
-val isnull_sign : 'a signature -> bool
-val hd_sign : 'a signature -> identifier * 'a
-val tl_sign : 'a signature -> 'a signature
-
-(* [sign_it f sign a] iters [f] on [sign] starting from [a] and
-   peeling [sign] from the oldest declaration *)
-
-val sign_it : (identifier -> 'a -> 'b -> 'b) -> 'a signature -> 'b -> 'b
-
-(* [it_sign f a sign] iters [f] on [sign] starting from [a] and
-   peeling [sign] from the more recent declaration *)
-
-val it_sign : ('b -> identifier -> 'a -> 'b) -> 'b -> 'a signature -> 'b
-
-val concat_sign : 'a signature -> 'a signature -> 'a signature
-
-val ids_of_sign : 'a signature -> identifier list
-val vals_of_sign : 'a signature -> 'a list
-
-val nth_sign : 'a signature -> int -> (identifier * 'a)
-val map_sign_graph : (identifier -> 'a -> 'b) -> 'a signature -> 'b list
-val list_of_sign : 'a signature -> (identifier * 'a) list
-val make_sign    : (identifier * 'a) list -> 'a signature
-val do_sign : (identifier -> 'a -> unit) -> 'a signature -> unit
-val uncons_sign : 'a signature -> (identifier * 'a) * 'a signature
-val sign_length : 'a signature -> int
-val mem_sign    : 'a signature -> identifier -> bool
-val modify_sign : identifier -> 'a -> 'a signature -> 'a signature
-
-val exists_sign : (identifier -> 'a -> bool) -> 'a signature -> bool
-val sign_prefix : identifier -> 'a signature -> 'a signature
-val add_sign_after : 
-  identifier -> (identifier * 'a) -> 'a signature -> 'a signature
-val add_sign_replacing : 
-  identifier -> (identifier * 'a) -> 'a signature -> 'a signature
-val prepend_sign : 'a signature -> 'a signature -> 'a signature
-
-val dunbind : identifier -> 'a signature -> 'a -> 'b term 
-  -> 'a signature * 'b term
-val dunbindv : identifier -> 'a signature -> 'a -> 'b term 
-  -> 'a signature * 'b term array
-val dbind : 'a signature -> 'b term -> 'a * 'b term
-val dbindv : 'a signature -> 'b term array -> 'a * 'b term
-
-(*s Signatures with named and de Bruijn variables. *)
-
-type 'a db_signature
-type ('a,'b) sign = ENVIRON of 'a signature * 'b db_signature
-
-val gLOB : 'b signature -> ('b,'a) sign
-
-val add_rel : (name * 'a) -> ('b,'a) sign -> ('b,'a) sign 
-val add_glob : (identifier * 'b) -> ('b,'a) sign -> ('b,'a) sign
-val lookup_glob : identifier -> ('b,'a) sign -> (identifier * 'b)
-val lookup_rel : int -> ('b,'a) sign  -> (name * 'a)
-val mem_glob : identifier -> ('b,'a) sign -> bool
-
-val nil_dbsign : 'a db_signature
-val get_globals : ('b,'a) sign -> 'b signature
-val get_rels : ('b,'a) sign -> 'a db_signature
-val dbenv_it : (name -> 'b -> 'c -> 'c) -> ('a,'b) sign -> 'c -> 'c
-val it_dbenv : ('c -> name -> 'b -> 'c) -> 'c -> ('a,'b) sign -> 'c
-val map_rel_env : ('a -> 'b) -> ('c,'a) sign -> ('c,'b) sign
-val map_var_env : ('c -> 'b) -> ('c,'a) sign -> ('b,'a) sign
-val isnull_rel_env : ('a,'b) sign -> bool
-val uncons_rel_env : ('a,'b) sign -> (name * 'b) * ('a,'b) sign
-val ids_of_env : ('a, 'b) sign -> identifier list
-val number_of_rels : ('b,'a) sign -> int
-
-(*i This is for Cases i*)
-(* raise [Not_found] if the integer is out of range *)
-val change_name_env: ('a, 'b) sign -> int -> identifier -> ('a, 'b) sign
-
-val make_all_name_different : ('a, 'b) sign -> ('a, 'b) sign
-
-type ('b,'a) search_result =
-  | GLOBNAME of identifier  * 'b
-  | RELNAME of int * 'a
-
-val lookup_id : identifier -> ('b,'a) sign -> ('b,'a) search_result
-
-
-type 'b assumptions = (typed_type,'b) sign
-type context = (typed_type,typed_type) sign
-type var_context = typed_type signature
-
-val unitize_env : 'a assumptions -> unit assumptions
-
-
-
-
-
-
-
+(*s Signatures of _ordered_ named variables, intended to be accessed by name *)
+
+type var_context = var_declaration list
+
+val add_var : identifier * constr option * typed_type -> var_context -> var_context
+val add_var_decl : identifier * typed_type -> var_context -> var_context
+val add_var_def : identifier * constr * typed_type -> var_context ->var_context
+val lookup_id : identifier -> var_context -> constr option * typed_type
+val lookup_id_type : identifier -> var_context -> typed_type
+val lookup_id_value : identifier -> var_context -> constr option 
+val pop_var : identifier -> var_context -> var_context
+val empty_var_context : var_context
+val ids_of_var_context : var_context -> identifier list
+val map_var_context : (constr -> constr) -> var_context -> var_context
+val mem_var_context : identifier -> var_context -> bool
+val fold_var_context : (var_declaration -> 'a -> 'a) -> var_context -> 'a -> 'a
+val fold_var_context_both_sides :
+  ('a -> var_declaration -> var_context -> 'a) -> var_context -> 'a -> 'a
+val it_var_context_quantifier :
+  (var_declaration -> constr -> constr) -> constr -> var_context -> constr
+val instantiate_sign : var_context -> constr list -> (identifier * constr) list
+val keep_hyps : Idset.t -> var_context -> var_context
+
+(*s Signatures of ordered optionally named variables, intended to be
+   accessed by de Bruijn indices *)
+
+type rel_context = rel_declaration list
+
+val add_rel : (name * constr option * typed_type) -> rel_context -> rel_context
+val add_rel_decl : (name * typed_type) -> rel_context -> rel_context
+val add_rel_def : (name * constr * typed_type) -> rel_context -> rel_context
+val lookup_rel_type : int -> rel_context -> name * typed_type
+val lookup_rel_value : int -> rel_context -> constr option
+val lookup_rel_id : identifier -> rel_context -> int * typed_type
+val empty_rel_context : rel_context
+val rel_context_length : rel_context -> int
+val lift_rel_context : int -> rel_context -> rel_context
+val concat_rel_context : newer:rel_context -> older:rel_context -> rel_context
+val ids_of_rel_context : rel_context -> identifier list
+val decls_of_rel_context : rel_context -> (name * constr) list
+val map_rel_context : (constr -> constr) -> rel_context -> rel_context
+
+(*s This is used to translate names into de Bruijn indices and
+   vice-versa without to care about typing information *)
+
+type names_context
+val add_name : name -> names_context -> names_context
+val lookup_name_of_rel : int -> names_context -> name
+val lookup_rel_of_name : identifier -> names_context -> int
+val names_of_rel_context : rel_context -> names_context
+val empty_names_context : names_context
+
+(*s Term destructors *)
+
+(* Transforms a product term $(x_1:T_1)..(x_n:T_n)T$ including letins
+   into the pair $([(x_n,T_n);...;(x_1,T_1)],T)$, where $T$ is not a
+   product nor a let. *)
+val decompose_prod_assum : constr -> rel_context * constr
+
+(* Transforms a lambda term $[x_1:T_1]..[x_n:T_n]T$ including letins
+   into the pair $([(x_n,T_n);...;(x_1,T_1)],T)$, where $T$ is not a
+   lambda nor a let. *)
+val decompose_lam_assum : constr -> rel_context * constr
+
+(* Given a positive integer n, transforms a product term 
+   $(x_1:T_1)..(x_n:T_n)T$
+   into the pair $([(xn,Tn);...;(x1,T1)],T)$. *)
+val decompose_prod_n_assum : int -> constr -> rel_context * constr
+
+(* Given a positive integer $n$, transforms a lambda term 
+   $[x_1:T_1]..[x_n:T_n]T$ into the pair $([(x_n,T_n);...;(x_1,T_1)],T)$ *)
+val decompose_lam_n_assum : int -> constr -> rel_context * constr
diff --git a/kernel/term.ml b/kernel/term.ml
index 8b5b05679..6b3aa5bec 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -107,6 +107,9 @@ let outcast_type x = x
 let typed_combine f g t u = f t u
 (**)
 
+type var_declaration = identifier * constr option * typed_type
+type rel_declaration = name * constr option * typed_type
+
 (****************************************************************************)
 (*              Functions for dealing with constr terms                     *)
 (****************************************************************************)
@@ -159,16 +162,53 @@ let mkCast t1 t2 =
 
 (* Constructs the product (x:t1)t2 *)
 let mkProd x t1 t2 = (DOP2 (Prod,t1,(DLAM (x,t2))))
-
-(* non-dependent product t1 -> t2 *)
-let mkArrow t1 t2 = mkProd Anonymous t1 t2
-
-(* named product *)
-let mkNamedProd name typ c = mkProd (Name name) typ (subst_var name c)
+let mkNamedProd id typ c = mkProd (Name id) typ (subst_var id c)
+let mkProd_string   s t c = mkProd (Name (id_of_string s)) t c
 
 (* Constructs the abstraction [x:t1]t2 *)
 let mkLambda x t1 t2 = (DOP2 (Lambda,t1,(DLAM (x,t2))))
-let mkNamedLambda name typ c = mkLambda (Name name) typ (subst_var name c)
+let mkNamedLambda id typ c = mkLambda (Name id) typ (subst_var id c)
+let mkLambda_string s t c = mkLambda (Name (id_of_string s)) t c
+
+(* Constructs [x=c_1:t]c_2 *)
+let mkLetIn x c1 t c2 = failwith "TODO"
+let mkNamedLetIn id c1 t c2 = mkLetIn (Name id) c1 t (subst_var id c2)
+
+(* Constructs either [(x:t)c] or [[x=b:t]c] *)
+let mkProd_or_LetIn (na,body,t) c =
+  match body with
+    | None -> mkProd na t c
+    | Some b -> mkLetIn na b t c
+
+let mkNamedProd_or_LetIn (id,body,t) c =
+  match body with
+    | None -> mkNamedProd id (body_of_type t) c
+    | Some b -> mkNamedLetIn id b (body_of_type t) c
+
+(* Constructs either [[x:t]c] or [[x=b:t]c] *)
+let mkLambda_or_LetIn (na,body,t) c =
+  match body with
+    | None -> mkLambda na t c
+    | Some b -> mkLetIn na b t c
+
+let mkNamedLambda_or_LetIn (id,body,t) c =
+  match body with
+    | None -> mkNamedLambda id (body_of_type t) c
+    | Some b -> mkNamedLetIn id b (body_of_type t) c
+
+(* Constructs either [(x:t)c] or [c] where [x] is replaced by [b] *)
+let mkProd_wo_LetIn (na,body,t) c =
+  match body with
+    | None -> mkProd na (body_of_type t) c
+    | Some b -> subst1 b c
+
+let mkNamedProd_wo_LetIn (id,body,t) c =
+  match body with
+    | None -> mkNamedProd id (body_of_type t) c
+    | Some b -> subst1 b (subst_var id c)
+
+(* non-dependent product t1 -> t2 *)
+let mkArrow t1 t2 = mkProd Anonymous t1 t2
 
 (* If lt = [t1; ...; tn], constructs the application (t1 ... tn) *)
 let mkAppL a = DOPN (AppL, a)
@@ -179,7 +219,7 @@ let mkAppList a l = DOPN (AppL, Array.of_list (a::l))
 let mkConst (sp,a) = DOPN (Const  sp, a)
 
 (* Constructs an existential variable *)
-let mkEvar n a = DOPN (Evar n, a)
+let mkEvar (n,a) = DOPN (Evar n, a)
 
 (* Constructs an abstract object *)
 let mkAbst sp a = DOPN (Abst sp, a)
@@ -215,9 +255,6 @@ let mkMutCaseA ci p c ac =
     with     fn [ctxn] = bn.
 
    where the lenght of the jth context is ij.
-
-   Warning: as an invariant the ti are casted during the Fix formation;
-   these casts are then used by destFix
 *)
 
 (* Here, we assume the body already constructed *)
@@ -509,10 +546,6 @@ let destCase = function
    where the lenght of the jth context is ij.
 *)
 
-let out_fixcast = function
-  | DOP2 (Cast, b, DOP0 (Sort s)) as c -> outcast_type c
-  | _ -> anomaly "destFix: malformed recursive definition"
-
 let destGralFix a =
   let nbofdefs = Array.length a in
   let types    = Array.sub a 0 (nbofdefs-1) in
@@ -529,26 +562,13 @@ let destGralFix a =
 let destFix = function 
   | DOPN (Fix (recindxs,i),a) -> 
       let (types,funnames,bodies) = destGralFix a in 
-      ((recindxs,i),((*Array.map out_fixcast *) types,funnames,bodies))
+      ((recindxs,i),(types,funnames,bodies))
   | _ -> invalid_arg "destFix"
 	
 let destCoFix = function 
   | DOPN ((CoFix i),a) ->
       let (types,funnames,bodies) = destGralFix a in
-      (i,((*Array.map out_fixcast *) types,funnames,bodies))
-  | _ -> invalid_arg "destCoFix"
-
-(* Provisoire, le temps de maitriser les cast *)
-let destUntypedFix = function 
-  | DOPN (Fix (recindxs,i),a) -> 
-      let (types,funnames,bodies) = destGralFix a in 
-      (recindxs,i,types,funnames,bodies)
-  | _ -> invalid_arg "destFix"
-
-let destUntypedCoFix = function 
-  | DOPN (CoFix i,a) -> 
-      let (types,funnames,bodies) = destGralFix a in 
-      (i,types,funnames,bodies)
+      (i,(types,funnames,bodies))
   | _ -> invalid_arg "destCoFix"
 
 (**********************************************************************)
@@ -636,9 +656,6 @@ let abs_implicit c = mkLambda Anonymous mkImplicit c
 let lambda_implicit a = mkLambda (Name(id_of_string"y")) mkImplicit a
 let lambda_implicit_lift n a = iterate lambda_implicit n (lift n a)
 
-let mkLambda_string s t c = mkLambda (Name (id_of_string s)) t c
-let mkProd_string   s t c = mkProd (Name (id_of_string s)) t c
-
 
 (* prod_it b [xn:Tn;..;x1:T1] = (x1:T1)..(xn:Tn)b *)
 let prod_it = List.fold_left (fun c (n,t)  -> mkProd n t c)
@@ -754,11 +771,11 @@ let rec isArity = function
    ([(xn,Tn);...;(x1,T1)],T), where T is not a product *)
 let decompose_prod = 
   let rec prodec_rec l = function
-    | DOP2(Prod,t,DLAM(x,c)) -> prodec_rec ((x,t)::l) c
+    | DOP2(Prod,t,DLAM(x,c)) ->	prodec_rec ((x,t)::l) c
     | DOP2(Cast,c,_)         -> prodec_rec l c
     | c                      -> l,c
   in 
-  prodec_rec [] 
+  prodec_rec []
 
 (* Transforms a lambda term [x1:T1]..[xn:Tn]T into the pair
    ([(xn,Tn);...;(x1,T1)],T), where T is not a lambda *)
@@ -768,7 +785,7 @@ let decompose_lam =
     | DOP2(Cast,c,_)         -> lamdec_rec l c
     | c                      -> l,c
   in 
-  lamdec_rec [] 
+  lamdec_rec []
 
 (* Given a positive integer n, transforms a product term (x1:T1)..(xn:Tn)T 
    into the pair ([(xn,Tn);...;(x1,T1)],T) *)
@@ -1306,13 +1323,14 @@ let rec subst_meta bl c =
    substitution is done the list may contain only negative occurrences
    that will not be substituted. *)
 
-let subst_term_occ locs c t = 
-  let rec substcheck except k occ c t =
+let subst_term_occ_gen locs occ c t =
+  let except = List.for_all (fun n -> n<0) locs in
+  let rec substcheck k occ c t =
     if except or List.exists (function u -> u>=occ) locs then
-      substrec except k occ c t
+      substrec k occ c t
     else 
       (occ,t)
-  and substrec except k occ c t =
+  and substrec k occ c t =
     if eq_constr t c then
       if except then 
 	if List.mem (-occ) locs then (occ+1,t) else (occ+1,Rel(k))
@@ -1327,44 +1345,60 @@ let subst_term_occ locs c t =
 	     let (occ',cl') =   
                Array.fold_left 
 		 (fun (nocc',lfd) f ->
-		    let (nocc'',f') = substcheck except k nocc' c f in
+		    let (nocc'',f') = substcheck k nocc' c f in
                     (nocc'',f'::lfd)) 
 		 (occ,[]) cl
              in 
 	     (occ',DOPN(i,Array.of_list (List.rev cl')))
 	|  DOP2(i,t1,t2) -> 
-	     let (nocc1,t1')=substrec except k occ c t1 in
-             let (nocc2,t2')=substcheck except k nocc1 c t2 in
+	     let (nocc1,t1')=substrec k occ c t1 in
+             let (nocc2,t2')=substcheck k nocc1 c t2 in
              nocc2,DOP2(i,t1',t2')
 	|  DOP1(i,t) -> 
-	     let (nocc,t')= substrec except k occ c t in
+	     let (nocc,t')= substrec k occ c t in
 	     nocc,DOP1(i,t')
 	|  DLAM(n,t) -> 
-	     let (occ',t') = substcheck except (k+1) occ (lift 1 c) t in
+	     let (occ',t') = substcheck (k+1) occ (lift 1 c) t in
              (occ',DLAM(n,t'))
 	|  DLAMV(n,cl) -> 
 	     let (occ',cl') =   
                Array.fold_left 
 		 (fun (nocc',lfd) f ->
 		    let (nocc'',f') = 
-		      substcheck except (k+1) nocc' (lift 1 c) f
+		      substcheck (k+1) nocc' (lift 1 c) f
                     in (nocc'',f'::lfd)) 
 		 (occ,[]) cl
              in 
 	     (occ',DLAMV(n,Array.of_list (List.rev cl') ))
 	|  _ -> occ,t
-  in 
-  if locs = [] then 
+  in
+  substcheck 1 occ c t
+
+let subst_term_occ locs c t = 
+  if locs = [] then
     subst_term c t
   else if List.mem 0 locs then 
     t
   else 
-    let except = List.for_all (fun n -> n<0) locs in
-    let (nbocc,t') = substcheck except 1 1 c t in
+    let (nbocc,t') = subst_term_occ_gen locs 1 c t in
     if List.exists (fun o -> o >= nbocc or o <= -nbocc) locs then
-      failwith "subst_term_occ: too few occurences";
+      errorlabstrm "subst_term_occ" [< 'sTR "Too few occurences" >];
     t'
 
+let subst_term_occ_decl locs c (id,bodyopt,typ as d) =
+  match bodyopt with
+    | None -> (id,None,subst_term_occ locs c typ)
+    | Some body -> 
+	if locs = [] then
+	  (id,Some (subst_term c body),typed_app (subst_term c) typ)
+	else if List.mem 0 locs then 
+	  d
+	else 
+	  let (nbocc,body') = subst_term_occ_gen locs 1 c body in
+	  let (nbocc',t') = typed_app (subst_term_occ_gen locs nbocc c) typ in
+	  if List.exists (fun o -> o >= nbocc' or o <= -nbocc') locs then
+	    errorlabstrm "subst_term_occ_decl" [< 'sTR "Too few occurences" >];
+	  (id,Some body',t')
   
 (***************************)
 (* occurs check functions  *)                         
diff --git a/kernel/term.mli b/kernel/term.mli
index 72ba6f511..9019fa091 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -59,10 +59,9 @@ type constr = sorts oper term
 
 type flat_arity = (name * constr) list * sorts
 
-type 'a judge = { body : constr; typ : 'a }
+(*type 'a judge = { body : constr; typ : 'a }*)
 
 type typed_type
-type typed_term = typed_type judge
 
 val make_typed : constr -> sorts -> typed_type
 val make_typed_lazy : constr -> (constr -> sorts) -> typed_type
@@ -78,6 +77,9 @@ val incast_type : typed_type -> constr
 
 val outcast_type : constr -> typed_type
 
+type var_declaration = identifier * constr option * typed_type
+type rel_declaration = name * constr option * typed_type
+
 (**********************************************************************)
 type binder_kind = BProd | BLambda
 
@@ -96,7 +98,10 @@ type 'ctxt reference =
   manipulation of terms. Some of these functions may be overlapped with
   previous ones. *)
 
-(*  Concrete type for making pattern-matching. *)
+(* Concrete type for making pattern-matching. *)
+
+(* [constr array] is an instance matching definitional var_context in
+   the same order (i.e. last argument first) *)
 type existential = int * constr array
 type constant = section_path * constr array
 type constructor = constructor_path * constr array
@@ -169,18 +174,30 @@ val implicit_sort : sorts
    type $t_2$ (that means t2 is declared as the type of t1). *)
 val mkCast : constr -> constr -> constr
 
-(* Constructs the product $(x:t_1)t_2$. $x$ may be anonymous. *)
+(* Constructs the product $(x:t_1)t_2$ *)
 val mkProd : name -> constr -> constr -> constr
-
-(* [mkProd_string s t c] constructs the product $(s:t)c$ *)
+val mkNamedProd : identifier -> constr -> constr -> constr
 val mkProd_string : string -> constr -> constr -> constr
 
+(* Constructs the product $(x:t_1)t_2$ *)
+val mkLetIn : name -> constr -> constr -> constr -> constr
+val mkNamedLetIn : identifier -> constr -> constr -> constr -> constr
+
+(* Constructs either [(x:t)c] or [[x=b:t]c] *)
+val mkProd_or_LetIn : rel_declaration -> constr -> constr
+val mkNamedProd_or_LetIn : var_declaration -> constr -> constr
+
+(* Constructs either [[x:t]c] or [[x=b:t]c] *)
+val mkLambda_or_LetIn : rel_declaration -> constr -> constr
+val mkNamedLambda_or_LetIn : var_declaration -> constr -> constr
+
+(* Constructs either [(x:t)c] or [c] where [x] is replaced by [b] *)
+val mkProd_wo_LetIn : rel_declaration -> constr -> constr
+val mkNamedProd_wo_LetIn : var_declaration -> constr -> constr
+
 (* non-dependant product $t_1 \rightarrow t_2$ *)
 val mkArrow : constr -> constr -> constr
 
-(* named product *)
-val mkNamedProd : identifier -> constr -> constr -> constr
-
 (* Constructs the abstraction $[x:t_1]t_2$ *)
 val mkLambda : name -> constr -> constr -> constr
 val mkNamedLambda : identifier -> constr -> constr -> constr
@@ -198,7 +215,7 @@ val mkAppList : constr -> constr list  -> constr
 val mkConst : constant -> constr
 
 (* Constructs an existential variable *)
-val mkEvar : int -> constr array -> constr
+val mkEvar : existential -> constr
 
 (* Constructs an abstract object *)
 val mkAbst : section_path -> constr array -> constr
@@ -360,13 +377,6 @@ val destFix : constr -> fixpoint
 
 val destCoFix : constr -> cofixpoint
 
-(* Provisoire, le temps de maitriser les cast *)
-val destUntypedFix : 
-  constr -> int array * int * constr array * Names.name list * constr array
-val destUntypedCoFix : 
-  constr -> int * constr array * Names.name list * constr array
-
-
 (*s Other term constructors. *)
 
 val abs_implicit : constr -> constr
@@ -410,7 +420,8 @@ val prod_applist : constr -> constr list -> constr
 (*s Other term destructors. *)
 
 (* Transforms a product term $(x_1:T_1)..(x_n:T_n)T$ into the pair
-   $([(x_n,T_n);...;(x_1,T_1)],T)$, where $T$ is not a product. *)
+   $([(x_n,T_n);...;(x_1,T_1)],T)$, where $T$ is not a product.
+   It includes also local definitions *)
 val decompose_prod : constr -> (name*constr) list * constr
 
 (* Transforms a lambda term $[x_1:T_1]..[x_n:T_n]T$ into the pair
@@ -420,11 +431,11 @@ val decompose_lam : constr -> (name*constr) list * constr
 (* Given a positive integer n, transforms a product term 
    $(x_1:T_1)..(x_n:T_n)T$
    into the pair $([(xn,Tn);...;(x1,T1)],T)$. *)
-val decompose_prod_n : int -> constr -> (name*constr) list * constr
+val decompose_prod_n : int -> constr -> (name * constr) list * constr
 
 (* Given a positive integer $n$, transforms a lambda term 
    $[x_1:T_1]..[x_n:T_n]T$ into the pair $([(x_n,T_n);...;(x_1,T_1)],T)$ *)
-val decompose_lam_n : int -> constr -> (name*constr) list * constr
+val decompose_lam_n : int -> constr -> (name * constr) list * constr
 
 (* [nb_lam] $[x_1:T_1]...[x_n:T_n]c$ where $c$ is not an abstraction
    gives $n$ (casts are ignored) *)
@@ -565,11 +576,16 @@ val rename_bound_var : identifier list -> constr -> constr
 val eta_reduce_head : constr -> constr
 val eq_constr : constr -> constr -> bool
 val eta_eq_constr : constr -> constr -> bool
-val subst_term : constr -> constr -> constr
-val subst_term_eta_eq : constr -> constr -> constr
+
+(*s The following functions substitutes [what] by [Rel 1] in [where] *)
+val subst_term : what:constr -> where:constr -> constr
+val subst_term_eta_eq : what:constr -> where:constr -> constr
+val subst_term_occ : occs:int list -> what:constr -> where:constr -> constr
+val subst_term_occ_decl : occs:int list -> what:constr ->
+      where:var_declaration -> var_declaration
+
 val replace_consts :
   (section_path * (identifier list * constr) option) list -> constr -> constr
-val subst_term_occ : int list -> constr -> constr -> constr
 
 (* [subst_meta bl c] substitutes the metavar $i$ by $c_i$ in [c] 
    for each binding $(i,c_i)$ in [bl],
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index d2891180a..14409c235 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -40,61 +40,59 @@ type type_error =
   | WrongPredicateArity of constr * int * int
   | NeedsInversion of constr * constr
 
-exception TypeError of path_kind * context * type_error
+exception TypeError of path_kind * env * type_error
 
-let context_ise sigma env =
-  map_var_env (typed_app (Reduction.nf_ise1 sigma))
-    (map_rel_env (typed_app (Reduction.nf_ise1 sigma))
-       (context env))
+let env_ise sigma env =
+  map_context (Reduction.nf_ise1 sigma) env
 
 let error_unbound_rel k env sigma n =
-  raise (TypeError (k, context_ise sigma env, UnboundRel n))
+  raise (TypeError (k, env_ise sigma env, UnboundRel n))
 
 let error_not_type k env c =
-  raise (TypeError (k, context env, NotAType c))
+  raise (TypeError (k, env, NotAType c))
 
 let error_assumption k env c =
-  raise (TypeError (k, context env, BadAssumption c))
+  raise (TypeError (k, env, BadAssumption c))
 
 let error_reference_variables k env id =
-  raise (TypeError (k, context env, ReferenceVariables id))
+  raise (TypeError (k, env, ReferenceVariables id))
 
 let error_elim_arity k env ind aritylst c p pt okinds = 
-  raise (TypeError (k, context env, ElimArity (ind,aritylst,c,p,pt,okinds)))
+  raise (TypeError (k, env, ElimArity (ind,aritylst,c,p,pt,okinds)))
 
 let error_case_not_inductive k env c ct = 
-  raise (TypeError (k, context env, CaseNotInductive (c,ct)))
+  raise (TypeError (k, env, CaseNotInductive (c,ct)))
 
 let error_number_branches k env c ct expn =
-  raise (TypeError (k, context env, NumberBranches (c,ct,expn)))
+  raise (TypeError (k, env, NumberBranches (c,ct,expn)))
 
 let error_ill_formed_branch k env c i actty expty =
-  raise (TypeError (k, context env, IllFormedBranch (c,i,actty,expty)))
+  raise (TypeError (k, env, IllFormedBranch (c,i,actty,expty)))
 
 let error_generalization k env sigma nvar c =
-  raise (TypeError (k, context_ise sigma env, Generalization (nvar,c)))
+  raise (TypeError (k, env_ise sigma env, Generalization (nvar,c)))
 
 let error_actual_type k env c actty expty =
-  raise (TypeError (k, context env, ActualType (c,actty,expty)))
+  raise (TypeError (k, env, ActualType (c,actty,expty)))
 
 let error_cant_apply_not_functional k env rator randl =
-  raise (TypeError (k, context env, CantApplyNonFunctional (rator,randl)))
+  raise (TypeError (k, env, CantApplyNonFunctional (rator,randl)))
 
 let error_cant_apply_bad_type k env sigma t rator randl =
-  raise(TypeError (k, context_ise sigma env, CantApplyBadType (t,rator,randl)))
+  raise(TypeError (k, env_ise sigma env, CantApplyBadType (t,rator,randl)))
 
 let error_ill_formed_rec_body k env str lna i vdefs =
-  raise (TypeError (k, context env, IllFormedRecBody (str,lna,i,vdefs)))
+  raise (TypeError (k, env, IllFormedRecBody (str,lna,i,vdefs)))
 
 let error_ill_typed_rec_body k env i lna vdefj vargs =
-  raise (TypeError (k, context env, IllTypedRecBody (i,lna,vdefj,vargs)))
+  raise (TypeError (k, env, IllTypedRecBody (i,lna,vdefj,vargs)))
 
 let error_not_inductive k env c =
-  raise (TypeError (k, context env, NotInductive c))
+  raise (TypeError (k, env, NotInductive c))
 
 let error_ml_case k env mes c ct br brt =
-  raise (TypeError (k, context env, MLCase (mes,c,ct,br,brt)))
+  raise (TypeError (k, env, MLCase (mes,c,ct,br,brt)))
 
 let error_not_product env c =
-  raise (TypeError (CCI, context env, NotProduct c))
+  raise (TypeError (CCI, env, NotProduct c))
 
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 38d6d8b6e..284f244f1 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -42,7 +42,7 @@ type type_error =
   | WrongPredicateArity of constr * int * int
   | NeedsInversion of constr * constr
 
-exception TypeError of path_kind * context * type_error
+exception TypeError of path_kind * env * type_error
 
 val error_unbound_rel : path_kind -> env -> 'a Evd.evar_map -> int -> 'b
 
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index a22e5715b..4077d852f 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -37,12 +37,11 @@ let type_judgment env sigma j =
 
 let assumption_of_type_judgment j = make_typed j.utj_val j.utj_type
 
-
 (* Type of a de Bruijn index. *)
 	  
 let relative env sigma n = 
   try
-    let (_,typ) = lookup_rel n env in
+    let (_,typ) = lookup_rel_type n env in
     { uj_val  = Rel n;
       uj_type = typed_app (lift n) typ }
   with Not_found -> 
@@ -51,13 +50,13 @@ let relative env sigma n =
 (* Management of context of variables. *)
 
 (* Checks if a context of variable is included in another one. *)
-
+(*
 let rec hyps_inclusion env sigma sign1 sign2 =
-  if isnull_sign sign1 then true
+  if sign1 = empty_var_context then true
   else
     let (id1,ty1) = hd_sign sign1 in
     let rec search sign2 =
-      if isnull_sign sign2 then false
+      if sign2 = empty_var_context then false
       else
 	let (id2,ty2) = hd_sign sign2 in
         if id1 = id2 then
@@ -68,15 +67,16 @@ let rec hyps_inclusion env sigma sign1 sign2 =
 	  search (tl_sign sign2)
     in 
     search sign2
+*)
 
 (* Checks if the given context of variables [hyps] is included in the
    current context of [env]. *)
-
+(*
 let check_hyps id env sigma hyps =
   let hyps' = var_context env in
   if not (hyps_inclusion env sigma hyps hyps') then
     error_reference_variables CCI env id
-
+*)
 (* Instantiation of terms on real arguments. *)
 
 let type_of_constant = Instantiate.constant_type
@@ -263,8 +263,11 @@ let sort_of_product_without_univ domsort rangsort =
            | Prop _ -> rangsort
            | Type u1 -> Type dummy_univ)
 
-let typed_product_without_universes name var c =
-  typed_combine (mkProd name) sort_of_product_without_univ var c
+let generalize_without_universes (_,_,var as d) c =
+  typed_combine
+    (fun _ c -> mkNamedProd_or_LetIn d c)
+    sort_of_product_without_univ
+    var c
 
 let typed_product env name var c =
   (* Gros hack ! *)
@@ -443,12 +446,11 @@ let is_subterm_specif env sigma lcx mind_recvec =
 	     stl.(0)
 	       
       | (DOPN(Fix(_),la) as mc,l) ->
-          let (recindxs,i,typarray,funnames,bodies) = destUntypedFix mc in
+          let ((recindxs,i),(typarray,funnames,bodies)) = destFix mc in
           let nbfix   = List.length funnames in
           let decrArg = recindxs.(i) in 
           let theBody = bodies.(i)   in
-          let (gamma,strippedBody) = decompose_lam_n (decrArg+1) theBody in
-          let absTypes = List.map snd gamma in 
+          let (_,strippedBody) = decompose_lam_n (decrArg+1) theBody in
           let nbOfAbst = nbfix+decrArg+1 in
           let newlst = 
             if List.length l < (decrArg+1) then
@@ -563,7 +565,7 @@ let rec check_subterm_rec_meta env sigma vectn k def =
 
 	| (DOPN(Fix(_),la) as mc,l) ->
             (List.for_all (check_rec_call n lst) l) &&
-            let (recindxs,i,typarray,funnames,bodies) = destUntypedFix mc in
+            let ((recindxs,i),(typarray,funnames,bodies)) = destFix mc in
             let nbfix = List.length funnames in
             let decrArg = recindxs.(i) in
             if (List.length l < (decrArg+1)) then
@@ -831,18 +833,4 @@ let control_only_guard env sigma =
   in 
   control_rec 
 
-(* [keep_hyps sign ids] keeps the part of the signature [sign] which 
-   contains the variables of the set [ids], and recursively the variables 
-   contained in the types of the needed variables. *)
-
-let keep_hyps sign needed =
-  rev_sign
-    (fst (it_sign 
-	    (fun ((hyps,globs) as sofar) id a ->
-               if Idset.mem id globs then
-                 (add_sign (id,a) hyps, 
-		  Idset.union (global_vars_set (body_of_type a)) globs)
-               else 
-		 sofar) 
-	    (nil_sign,needed) sign))
     
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 6d1faa0ff..a07206fb0 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -51,8 +51,7 @@ val judge_of_prop_contents : contents -> unsafe_judgment
 
 val judge_of_type : universe -> unsafe_judgment * constraints
 
-val typed_product_without_universes :
-  name -> typed_type -> typed_type -> typed_type
+val generalize_without_universes : var_declaration -> typed_type -> typed_type
 
 val abs_rel : 
   env -> 'a evar_map -> name -> typed_type -> unsafe_judgment 
@@ -85,6 +84,7 @@ open Inductive
 val find_case_dep_nparams :
   env -> 'a evar_map -> constr * constr -> inductive_family -> constr -> bool
 
+(*
 val hyps_inclusion : env -> 'a evar_map -> var_context -> var_context -> bool
+*)
 
-val keep_hyps : var_context -> Idset.t -> var_context