Renommage canonique :

declaration = definition | assumption
mode de reference = named | rel

Ex:
push_named_decl : named_declaration -> env -> env
lookup_named : identifier -> safe_environment -> constr option * typed_type
add_named_assum : identifier * typed_type -> named_context -> named_context
add_named_def : identifier*constr*typed_type -> named_context -> named_context


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

19 files changed, 216 insertions, 229 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 71bfa0778f..ae5e51db0f 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -294,7 +294,7 @@ let make_constr_ref n = function
 
 let defined_vars flags env =
   if red_local_const (snd flags) then
-    fold_var_context 
+    fold_named_context 
       (fun env (id,b,t) e ->
 	 match b with
 	   | None -> e
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 82ad0583ce..3b2ba2ecef 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 : var_context;
+  const_hyps : named_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 : var_context;
+  mind_hyps : named_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 65f70e2776..3a85e7e05f 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -8,6 +8,9 @@ open Term
 open Sign
 (*i*)
 
+(* This module defines the types of global declarations. This includes
+   global constants/axioms and mutual inductive definitions *)
+
 (*s Constants (internal representation) (Definition/Axiom) *)
 
 type lazy_constant_value =
@@ -20,7 +23,7 @@ type constant_body = {
   const_kind : path_kind;
   const_body : constant_value option;
   const_type : typed_type;
-  const_hyps : var_context; (* New: younger hyp at top *)
+  const_hyps : named_context; (* New: younger hyp at top *)
   const_constraints : constraints;
   mutable const_opaque : bool }
 
@@ -66,7 +69,7 @@ type one_inductive_body = {
 type mutual_inductive_body = {
   mind_kind : path_kind;
   mind_ntypes : int;
-  mind_hyps : var_context;
+  mind_hyps : named_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 bce436ade1..45ec56816a 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -25,7 +25,7 @@ type globals = {
   env_imports : import list }
 
 type context = {
-  env_var_context : var_context;
+  env_named_context : named_context;
   env_rel_context : rel_context }
 
 type env = {
@@ -34,7 +34,7 @@ type env = {
   env_universes : universes }
 
 let empty_context = {
-  env_var_context = empty_var_context;
+  env_named_context = empty_named_context;
   env_rel_context = empty_rel_context }
   
 let empty_env = { 
@@ -48,7 +48,7 @@ let empty_env = {
 
 let universes env = env.env_universes
 let context env = env.env_context
-let var_context env = env.env_context.env_var_context
+let named_context env = env.env_context.env_named_context
 let rel_context env = env.env_context.env_rel_context
 
 (* Construction functions. *)
@@ -58,20 +58,20 @@ let map_context f env =
   { env with
       env_context = {
 	context with
-	  env_var_context = map_var_context f context.env_var_context ;
+	  env_named_context = map_named_context f context.env_named_context ;
 	  env_rel_context = map_rel_context f context.env_rel_context } }
 
-let var_context_app f env =
+let named_context_app f env =
   { env with
       env_context = { env.env_context with
-			env_var_context = f env.env_context.env_var_context } }
+			env_named_context = f env.env_context.env_named_context } }
 
-let change_hyps = var_context_app
+let change_hyps = named_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 push_named_decl d   = named_context_app (add_named_decl d)
+let push_named_def def   = named_context_app (add_named_def def)
+let push_named_assum decl = named_context_app (add_named_assum decl)
+let pop_named_decl id         = named_context_app (pop_named_decl id)
 
 let rel_context_app f env =
   { env with
@@ -80,51 +80,51 @@ let rel_context_app f env =
 
 let reset_context env =
   { env with
-      env_context = { env_var_context = empty_var_context;
+      env_context = { env_named_context = empty_named_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 fold_named_context f env a =
+  snd (Sign.fold_named_context
+	 (fun d (env,e) -> (push_named_decl d env, f env d e))
+         (named_context env) (reset_context env,a))
 
-let fold_var_context_reverse f a env =
-  Sign.fold_var_context_reverse f a (var_context env) 
+let fold_named_context_reverse f a env =
+  Sign.fold_named_context_reverse f a (named_context env) 
 
-let process_var_context f env =
-  Sign.fold_var_context
-    (fun d env -> f env d) (var_context env) (reset_context env)
+let process_named_context f env =
+  Sign.fold_named_context
+    (fun d env -> f env d) (named_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 process_named_context_both_sides f env =
+  fold_named_context_both_sides f (named_context env) (reset_context env)
 
-let push_rel d   = rel_context_app (add_rel d)
+let push_rel d   = rel_context_app (add_rel_decl 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_rel_assum decl = rel_context_app (add_rel_assum 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 push_rel_context_to_named_context env =
+  let sign0 = env.env_context.env_named_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
        ((mkVar id)::subst,id::avoid,
-	add_var (id,option_app (substl subst) c,typed_app (substl subst) t)
+	add_named_decl (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)
+    env.env_context.env_rel_context ([],ids_of_named_context sign0,sign0)
+  in subst, (named_context_app (fun _ -> sign) env)
 
 let push_rec_types (typarray,names,_) env =
   let vect_lift_type = Array.mapi (fun i t -> outcast_type (lift i t)) in
   let nlara = 
     List.combine (List.rev names) (Array.to_list (vect_lift_type typarray)) in
-  List.fold_left (fun env nvar -> push_rel_decl nvar env) env nlara
+  List.fold_left (fun env nvar -> push_rel_assum nvar env) env nlara
 
 let reset_rel_context env =
   { env with
-      env_context = { env_var_context = env.env_context.env_var_context;
+      env_context = { env_named_context = env.env_context.env_named_context;
 		      env_rel_context = empty_rel_context} }
 
 let fold_rel_context f env a =
@@ -136,11 +136,11 @@ 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 instantiate_named_context  = 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)
+  @ (ids_of_named_context env.env_context.env_named_context)
 
 let names_of_rel_context env =
   names_of_rel_context env.env_context.env_rel_context
@@ -178,13 +178,13 @@ let new_meta ()=incr meta_ctr;!meta_ctr;;
 
 (* Access functions. *)
   
-let lookup_var_type id env =
-  lookup_id_type id env.env_context.env_var_context
+let lookup_named_type id env =
+  lookup_id_type id env.env_context.env_named_context
 
-let lookup_var_value id env =
-  lookup_id_value id env.env_context.env_var_context
+let lookup_named_value id env =
+  lookup_id_value id env.env_context.env_named_context
 
-let lookup_var id env = lookup_id id env.env_context.env_var_context
+let lookup_named id env = lookup_id id env.env_context.env_named_context
 
 let lookup_rel_type n env =
   Sign.lookup_rel_type n env.env_context.env_rel_context
@@ -288,11 +288,11 @@ let it_mkProd_wo_LetIn   = List.fold_left (fun c d -> mkProd_wo_LetIn d c)
 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 it_mkNamedProd_or_LetIn = it_named_context_quantifier mkNamedProd_or_LetIn
+let it_mkNamedLambda_or_LetIn = it_named_context_quantifier mkNamedLambda_or_LetIn
 
 let make_all_name_different env =
-  let avoid = ref (ids_of_var_context (var_context env)) in
+  let avoid = ref (ids_of_named_context (named_context env)) in
   process_rel_context
     (fun newenv (na,c,t) -> 
        let id = next_name_away na !avoid in
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 30d93a02e4..611987c90b 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -23,50 +23,48 @@ 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 named_context : env -> named_context
 
-(* This forgets var and rel contexts *)
+(* This forgets named 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] *)
+(*s This concerns only local vars referred by names [named_context] *)
+val push_named_decl : named_declaration -> env -> env
+val push_named_assum : identifier * typed_type -> env -> env
+val push_named_def : identifier * constr * typed_type -> env -> env
+val change_hyps : (named_context -> named_context) -> env -> env
+val instantiate_named_context  : named_context -> constr list -> (identifier * constr) list
+val pop_named_decl : identifier -> env -> env
+
+(*s This concerns only 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_assum : 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
+val push_rel_context_to_named_context : env -> constr list * env
 
 (*s Push the types of a (co-)fixpoint *)
 val push_rec_types : rec_declaration -> env -> env
 
-(* Gives identifiers in [var_context] and [rel_context] *)
+(* Gives identifiers in [named_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
+(*s Recurrence on [named_context] *)
+val fold_named_context : (env -> named_declaration -> 'a -> 'a) -> env -> 'a -> 'a
+val process_named_context : (env -> named_declaration -> env) -> env -> env
 
-(* Recurrence on [var_context] starting from younger decl *)
-val fold_var_context_reverse : ('a -> var_declaration -> 'a) -> 'a -> env -> 'a
+(* Recurrence on [named_context] starting from younger decl *)
+val fold_named_context_reverse : ('a -> named_declaration -> 'a) -> 'a -> env -> 'a
 
-(* [process_var_context_both_sides f env] iters [f] on the var
+(* [process_named_context_both_sides f env] iters [f] on the named
    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 
+val process_named_context_both_sides :
+  (env -> named_declaration -> named_context -> env) -> env -> env 
 
 (*s Recurrence on [rel_context] *)
 val fold_rel_context : (env -> rel_declaration -> 'a -> 'a) -> env -> 'a -> 'a
@@ -83,11 +81,11 @@ val new_meta : unit -> int
 
 (*s Looks up in environment *)
 
-(* Looks up in the context of local vars referred by names ([var_context]) *)
+(* Looks up in the context of local vars referred by names ([named_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
+val lookup_named_type : identifier -> env -> typed_type
+val lookup_named_value : identifier -> env -> constr option
+val lookup_named : 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 *)
@@ -136,8 +134,8 @@ val it_mkProd_wo_LetIn : 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
+val it_mkNamedLambda_or_LetIn : constr -> named_context -> constr
+val it_mkNamedProd_or_LetIn : constr -> named_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
diff --git a/kernel/evd.ml b/kernel/evd.ml
index b482f94538..64602f870c 100644
--- a/kernel/evd.ml
+++ b/kernel/evd.ml
@@ -65,7 +65,7 @@ let is_defined sigma ev =
   let info = map sigma ev in 
   not (info.evar_body = Evar_empty)
 
-let evar_hyps ev = var_context ev.evar_env
+let evar_hyps ev = named_context ev.evar_env
 let evar_body ev = ev.evar_body
 
 let id_of_existential ev =
diff --git a/kernel/evd.mli b/kernel/evd.mli
index 4315994964..e744748358 100644
--- a/kernel/evd.mli
+++ b/kernel/evd.mli
@@ -48,7 +48,7 @@ val is_evar : 'a evar_map -> evar -> bool
 
 val is_defined : 'a evar_map -> evar -> bool
 
-val evar_hyps : 'a evar_info -> var_context
+val evar_hyps : 'a evar_info -> named_context
 val evar_body : 'a evar_info -> evar_body
 
 val id_of_existential : evar -> identifier
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index a5ca14f522..fdfdf0052e 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -180,7 +180,7 @@ let listrec_mconstr env ntypes nparams i indlc =
 	  assert (largs = []);
           if not (noccur_between n ntypes b) then
 	    raise (IllFormedInd (LocalNonPos n));
-	  check_pos (push_rel_decl (na, outcast_type b) env) (n+1) d
+	  check_pos (push_rel_assum (na, outcast_type b) env) (n+1) d
       | IsRel k ->
           if k >= n && k<n+ntypes then begin
 	    check_correct_par env nparams ntypes n (k-n+1) largs;
@@ -246,7 +246,7 @@ let listrec_mconstr env ntypes nparams i indlc =
       (* The extra case *)
       | IsLambda (na,b,d) -> 
           if noccur_between n ntypes b
-          then check_weak_pos (push_rel_decl (na,outcast_type b) env) (n+1) d
+          then check_weak_pos (push_rel_assum (na,outcast_type b) env) (n+1) d
           else raise (IllFormedInd (LocalNonPos n))
       (******************)
       | _ -> check_pos env n x
@@ -263,7 +263,7 @@ let listrec_mconstr env ntypes nparams i indlc =
         | IsProd (na,b,d) -> 
 	    assert (largs = []);
             let recarg = check_pos env n b in 
-	    check_constr_rec (push_rel_decl (na,outcast_type b) env)
+	    check_constr_rec (push_rel_assum (na,outcast_type b) env)
 	      (recarg::lrec) (n+1) d
 
         (* LetIn's must be free of occurrence of the inductive types and
@@ -358,7 +358,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 ids (var_context env);
+    mind_hyps = keep_hyps ids (named_context env);
     mind_packets = packets;
     mind_constraints = cst;
     mind_singl = None;
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index 7888afd390..ab818d0e52 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -19,7 +19,7 @@ let is_id_inst inst =
   List.for_all is_id inst
 
 let instantiate_constr sign c args =
-  let inst = instantiate_vars sign args in
+  let inst = instantiate_named_context  sign args in
   if is_id_inst inst then
     c
   else
diff --git a/kernel/instantiate.mli b/kernel/instantiate.mli
index f0719d2f1e..f905ca27ee 100644
--- a/kernel/instantiate.mli
+++ b/kernel/instantiate.mli
@@ -12,9 +12,9 @@ open Environ
 (* Instantiation of constants and inductives on their real arguments. *)
 
 val instantiate_constr : 
-  var_context -> constr -> constr list -> constr
+  named_context -> constr -> constr list -> constr
 val instantiate_type : 
-  var_context -> typed_type -> constr list -> typed_type
+  named_context -> typed_type -> constr list -> typed_type
 
 (*s [constant_value env c] raises [NotEvaluableConst Opaque] if
    [c] is opaque and [NotEvaluableConst NoBody] if it has no
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index bfb3a565fd..3306927d6e 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -277,7 +277,7 @@ let whd_state_gen flags env sigma =
 	     | Some body -> whrec (lift n body, stack)
 	     | None -> s)
       | IsVar id when red_delta flags ->
-	  (match lookup_var_value id env with
+	  (match lookup_named_value id env with
 	     | Some body -> whrec (body, stack)
 	     | None -> s)
 *)
@@ -975,7 +975,7 @@ let splay_prod env sigma =
     let t = whd_betadeltaiota env sigma c in
     match kind_of_term t with
       | IsProd (n,a,c0) ->
-	  decrec (push_rel_decl (n,outcast_type a) env)
+	  decrec (push_rel_assum (n,outcast_type a) env)
 	    ((n,a)::m) c0
       | _ -> m,t
   in 
@@ -986,8 +986,8 @@ let splay_prod_assum env sigma =
     let t = whd_betadeltaiota_nolet env sigma c in
     match kind_of_term c with
     | IsProd (x,t,c)  ->
-	prodec_rec (push_rel_decl (x,outcast_type t) env)
-	  (Sign.add_rel_decl (x,outcast_type t) l) c
+	prodec_rec (push_rel_assum (x,outcast_type t) env)
+	  (Sign.add_rel_assum (x,outcast_type t) l) c
     | IsLetIn (x,b,t,c) ->
 	prodec_rec (push_rel_def (x,b,outcast_type t) env)
 	  (Sign.add_rel_def (x,b,outcast_type t) l) c
@@ -1009,8 +1009,8 @@ let decomp_n_prod env sigma n =
     match kind_of_term (whd_betadeltaiota env sigma c) with
       | IsProd (n,a,c0) ->
 	  let a = make_typed_lazy a (fun _ -> Type dummy_univ) in
-	  decrec (push_rel_decl (n,a) env)
-	    (m-1) (Sign.add_rel_decl (n,a) ln) c0
+	  decrec (push_rel_assum (n,a) env)
+	    (m-1) (Sign.add_rel_assum (n,a) ln) c0
       | _                      -> error "decomp_n_prod: Not enough products"
   in 
   decrec env n Sign.empty_rel_context
@@ -1078,8 +1078,8 @@ let find_conclusion env sigma =
   let rec decrec env c =
     let t = whd_betadeltaiota env sigma c in
     match kind_of_term t with
-      | IsProd (x,t,c0) -> decrec (push_rel_decl (x,outcast_type t) env) c0
-      | IsLambda (x,t,c0) -> decrec (push_rel_decl (x,outcast_type t) env) c0
+      | IsProd (x,t,c0) -> decrec (push_rel_assum (x,outcast_type t) env) c0
+      | IsLambda (x,t,c0) -> decrec (push_rel_assum (x,outcast_type t) env) c0
       | t -> t
   in 
   decrec env
@@ -1135,12 +1135,12 @@ let poly_args env sigma t =
     match kind_of_term (whd_betadeltaiota env sigma t) with
       | IsProd (x,a,b) ->
 	  add_free_rels_until n a
-	    (aux (push_rel_decl (x,outcast_type a) env) (n+1) b)
+	    (aux (push_rel_assum (x,outcast_type a) env) (n+1) b)
       | _ -> Intset.empty
   in 
   match kind_of_term (whd_betadeltaiota env sigma t) with 
     | IsProd (x,a,b) ->
-	Intset.elements (aux (push_rel_decl (x,outcast_type a) env) 1 b)
+	Intset.elements (aux (push_rel_assum (x,outcast_type a) env) 1 b)
     | _ -> []
 
 (* Expanding existential variables (pretyping.ml) *)
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 75e7cd70df..a62bc962a8 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 (lookup_var_type id env), cst0)
+	(make_judge cstr (lookup_named_type id env), cst0)
 
     (* ATTENTION : faudra faire le typage du contexte des Const,
     MutInd et MutConstructsi un jour cela devient des constructions
@@ -104,7 +104,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_decl (name,var) env in
+	let env1 = push_rel_assum (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
@@ -113,7 +113,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_decl (name,assumption_of_type_judgment varj) env in
+	let env1 = push_rel_assum (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
@@ -143,7 +143,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_decl nvar env) env nlara in
+    List.fold_left (fun env nvar -> push_rel_assum 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
@@ -233,11 +233,11 @@ let empty_environment = empty_env
 
 let universes = universes
 let context = context
-let var_context = var_context
+let named_context = named_context
 
-let lookup_var_type = lookup_var_type
+let lookup_named_type = lookup_named_type
 let lookup_rel_type = lookup_rel_type
-let lookup_var = lookup_var
+let lookup_named = lookup_named
 let lookup_constant = lookup_constant
 let lookup_mind = lookup_mind
 let lookup_mind_specif = lookup_mind_specif
@@ -245,27 +245,25 @@ 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_def push (id,c) env =
-  let (j,cst) = safe_infer env c in
+let push_rel_or_named_def push (id,b) env =
+  let (j,cst) = safe_infer env b in
   let env' = add_constraints cst env in
   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_named_def = push_rel_or_named_def push_named_def
+let push_rel_def = push_rel_or_named_def push_rel_def
 
-let push_rel_def nrel env = push_rel_or_var_def push_rel_def nrel env
-
-let push_rel_or_var_decl push (id,c) env =
-  let (j,cst) = safe_infer_type env c in
+let push_rel_or_named_assum push (id,t) env =
+  let (j,cst) = safe_infer env t in
   let env' = add_constraints cst env in
-  let var = assumption_of_type_judgment j in
-  push (id,var) env'
-
-let push_var_decl nvar env = push_rel_or_var_decl push_var_decl nvar env
+  let t = assumption_of_judgment env Evd.empty j in
+  push (id,t) env'
 
-let push_rel_decl nrel env = push_rel_or_var_decl push_rel_decl nrel env
+let push_named_assum = push_rel_or_named_assum push_named_assum
+let push_rel_assum = push_rel_or_named_assum push_rel_assum
 
 let push_rels_with_univ vars env =
-  List.fold_left (fun env nvar -> push_rel_decl nvar env) env vars
+  List.fold_left (fun env nvar -> push_rel_assum nvar env) env vars
 
 (* Insertion of constants and parameters in environment. *)
 
@@ -294,7 +292,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 ids (var_context env);
+    const_hyps = keep_hyps ids (named_context env);
     const_constraints = Constraint.union cst cst';
     const_opaque = false } 
   in
@@ -308,7 +306,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 ids (var_context env);
+    const_hyps = keep_hyps ids (named_context env);
     const_constraints = cst;
     const_opaque = false } 
   in
@@ -330,7 +328,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 ids (var_context env);
+    const_hyps = keep_hyps ids (named_context env);
     const_constraints = cst;
     const_opaque = false } 
   in
@@ -355,7 +353,7 @@ let rec infos_and_sort env t =
     | IsProd (name,c1,c2) ->
         let (varj,_) = safe_infer_type env c1 in
 	let var = assumption_of_type_judgment varj in
-	let env1 = Environ.push_rel_decl (name,var) env in
+	let env1 = Environ.push_rel_assum (name,var) env in
 	let s1 = varj.utj_type in
 	let logic = not (is_info_type env Evd.empty varj) in
 	let small = is_small s1 in
@@ -453,10 +451,10 @@ let add_mind sp mie env =
     
 let add_constraints = add_constraints
 
-let rec pop_vars idl env =
+let rec pop_named_decls idl env =
   match idl with 
     | [] -> env
-    | id::l -> pop_vars l (Environ.pop_var id env)
+    | id::l -> pop_named_decls l (Environ.pop_named_decl id env)
 
 let export = export
 let import = import
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 577f753d37..a07be1fca6 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -24,14 +24,12 @@ val empty_environment : safe_environment
 
 val universes : safe_environment -> universes
 val context : safe_environment -> context
-val var_context : safe_environment -> var_context
+val named_context : safe_environment -> named_context
 
-val push_var_decl : identifier * constr -> safe_environment -> safe_environment
-val push_var_def : identifier * constr -> safe_environment -> safe_environment
-(*i
-val push_rel_decl : name * constr -> safe_environment -> safe_environment
-val push_rel_def : name * constr -> safe_environment -> safe_environment
-i*)
+val push_named_assum :
+  identifier * constr -> safe_environment -> safe_environment
+val push_named_def :
+  identifier * constr -> safe_environment -> safe_environment
 
 val add_constant : 
   section_path -> constant_entry -> safe_environment -> safe_environment
@@ -45,9 +43,9 @@ val add_mind :
     -> safe_environment
 val add_constraints : constraints -> safe_environment -> safe_environment
 
-val pop_vars : identifier list -> safe_environment -> safe_environment
+val pop_named_decls : identifier list -> safe_environment -> safe_environment
 
-val lookup_var : identifier -> safe_environment -> constr option * typed_type
+val lookup_named : identifier -> safe_environment -> constr option * typed_type
 (*i
 val lookup_rel : int -> safe_environment -> name * typed_type
 i*)
diff --git a/kernel/sign.ml b/kernel/sign.ml
index d9438eb98a..4a8078ef4b 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -14,12 +14,12 @@ 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
+type named_declaration = identifier * constr option * typed_type
+type named_context = named_declaration list
 
-let add_var = add
-let add_var_decl = add_decl
-let add_var_def = add_def
+let add_named_decl = add
+let add_named_assum = add_decl
+let add_named_def = add_def
 let rec lookup_id_type id = function
   | (id',c,t) :: _ when id=id' -> t
   | _ :: sign -> lookup_id_type id sign
@@ -32,26 +32,26 @@ 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
+let empty_named_context = []
+let pop_named_decl 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
+let ids_of_named_context = List.map (fun (id,_,_) -> id)
+let map_named_context = map
+let rec mem_named_context id = function
   | (id',_,_) :: _ when id=id' -> true
-  | _ :: sign -> mem_var_context id sign
+  | _ :: sign -> mem_named_context id sign
   | [] -> false
-let fold_var_context = List.fold_right
-let fold_var_context_reverse = List.fold_left
-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)
+let fold_named_context = List.fold_right
+let fold_named_context_reverse = List.fold_left
+let fold_named_context_both_sides = list_fold_right_and_left
+let it_named_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_decl = add
+let add_rel_assum = add_decl
 let add_rel_def = add_def
 let lookup_rel_type n sign =
   let rec lookrec = function
@@ -90,7 +90,7 @@ let ids_of_rel_context sign =
     (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 =
+let assums_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 []
@@ -149,7 +149,7 @@ let empty_names_context = []
 let decompose_prod_assum = 
   let rec prodec_rec l c =
     match kind_of_term c with
-    | IsProd (x,t,c)  -> prodec_rec (add_rel_decl (x,outcast_type t) l) c
+    | IsProd (x,t,c)  -> prodec_rec (add_rel_assum (x,outcast_type t) l) c
     | IsLetIn (x,b,t,c) -> prodec_rec (add_rel_def (x,b,outcast_type t) l) c
     | IsCast (c,_)    -> prodec_rec l c
     | _               -> l,c
@@ -161,7 +161,7 @@ let decompose_prod_assum =
 let decompose_lam_assum = 
   let rec lamdec_rec l c =
     match kind_of_term c with
-    | IsLambda (x,t,c) -> lamdec_rec (add_rel_decl (x,outcast_type t) l) c
+    | IsLambda (x,t,c) -> lamdec_rec (add_rel_assum (x,outcast_type t) l) c
     | IsLetIn (x,b,t,c) -> lamdec_rec (add_rel_def (x,b,outcast_type t) l) c
     | IsCast (c,_)     -> lamdec_rec l c
     | _                -> l,c
@@ -175,7 +175,7 @@ let decompose_prod_n_assum n =
   let rec prodec_rec l n c = 
     if n=0 then l,c 
     else match kind_of_term c with 
-    | IsProd (x,t,c) -> prodec_rec (add_rel_decl(x,outcast_type t) l) (n-1) c
+    | IsProd (x,t,c) -> prodec_rec (add_rel_assum(x,outcast_type t) l) (n-1) c
     | IsLetIn (x,b,t,c) ->
 	prodec_rec (add_rel_def (x,b,outcast_type t) l) (n-1) c
     | IsCast (c,_)   -> prodec_rec l n c
@@ -190,7 +190,7 @@ let decompose_lam_n_assum n =
   let rec lamdec_rec l n c = 
     if n=0 then l,c 
     else match kind_of_term c with 
-    | IsLambda (x,t,c) -> lamdec_rec (add_rel_decl (x,outcast_type t) l) (n-1) c
+    | IsLambda (x,t,c) -> lamdec_rec (add_rel_assum (x,outcast_type t) l) (n-1) c
     | IsLetIn (x,b,t,c) ->
 	lamdec_rec (add_rel_def (x,b,outcast_type t) l) (n-1) c
     | IsCast (c,_)     -> lamdec_rec l n c
diff --git a/kernel/sign.mli b/kernel/sign.mli
index 30e1dae28d..51e8107448 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -7,39 +7,42 @@ open Names
 open Term
 (*i*)
 
-(*s Signatures of ordered named variables, intended to be accessed by name *)
+(*s Signatures of ordered named declarations *)
 
-type var_context = var_declaration list
+type named_context = named_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_reverse : ('a -> var_declaration -> 'a) -> 'a -> var_context -> '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
+val add_named_decl : 
+  identifier * constr option * typed_type -> named_context -> named_context
+val add_named_assum : identifier * typed_type -> named_context -> named_context
+val add_named_def : 
+  identifier * constr * typed_type -> named_context -> named_context
+val lookup_id : identifier -> named_context -> constr option * typed_type
+val lookup_id_type : identifier -> named_context -> typed_type
+val lookup_id_value : identifier -> named_context -> constr option 
+val pop_named_decl : identifier -> named_context -> named_context
+val empty_named_context : named_context
+val ids_of_named_context : named_context -> identifier list
+val map_named_context : (constr -> constr) -> named_context -> named_context
+val mem_named_context : identifier -> named_context -> bool
+val fold_named_context :
+  (named_declaration -> 'a -> 'a) -> named_context -> 'a -> 'a
+val fold_named_context_reverse :
+  ('a -> named_declaration -> 'a) -> 'a -> named_context -> 'a
+val fold_named_context_both_sides :
+  ('a -> named_declaration -> named_context -> 'a) -> named_context -> 'a -> 'a
+val it_named_context_quantifier :
+  (named_declaration -> constr -> constr) -> constr -> named_context -> constr
+val instantiate_sign :
+  named_context -> constr list -> (identifier * constr) list
+val keep_hyps : Idset.t -> named_context -> named_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_decl : (name * constr option * typed_type) -> rel_context -> rel_context
+val add_rel_assum : (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
@@ -49,7 +52,7 @@ 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 assums_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
diff --git a/kernel/term.ml b/kernel/term.ml
index b70bb05a07..81fbd9a02e 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -784,7 +784,7 @@ let outcast_type x = x
 let typed_combine f g t u = f t u
 (**)
 
-type var_declaration = identifier * constr option * typed_type
+type named_declaration = identifier * constr option * typed_type
 type rel_declaration = name * constr option * typed_type
 
 
diff --git a/kernel/term.mli b/kernel/term.mli
index f2a49e838f..40bc12ce3d 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -35,29 +35,6 @@ type case_printing =
 (* the integer is the number of real args, needed for reduction *)
 type case_info = int array * case_printing
 
-(*
-type 'a oper = 
-  | Meta of int
-  | Sort of 'a
-  | Cast | Prod | Lambda
-  | AppL | Const of section_path
-  | Evar of existential_key
-  | MutInd of inductive_path
-  | MutConstruct of constructor_path
-  | MutCase of case_info
-  | Fix of int array * int
-  | CoFix of int
-  | XTRA of string
-*)
-
-(*s The type [constr] of the terms of CCI
-  is obtained by instanciating a generic notion of terms
-  on the above operators, themselves instanciated
-  on the above sorts. *)
-
-(* [VAR] is used for named variables and [Rel] for variables as
-   de Bruijn indices. *)
-
 type constr
 
 type typed_type
@@ -78,12 +55,20 @@ val incast_type : typed_type -> constr
 
 val outcast_type : constr -> typed_type
 
-type var_declaration = identifier * constr option * typed_type
+(*s A {\em declaration} has the form (name,body,type). It is either an
+    {\em assumption} if [body=None] or a {\em definition} if
+    [body=Some actualbody]. It is referred by {\em name} if [na] is an
+    identifier or by {\em relative index} if [na] is not an identifier
+    (in the latter case, [na] is of type [name] but just for printing
+    purpose *)
+
+type named_declaration = identifier * constr option * typed_type
 type rel_declaration = name * constr option * typed_type
 
 type arity = rel_declaration list * sorts
 
-(**********************************************************************)
+(*i********************************************************************i*)
+(*s type of global reference *)
 type global_reference =
   | ConstRef of section_path
   | IndRef of inductive_path
@@ -96,7 +81,7 @@ type global_reference =
 
 (* Concrete type for making pattern-matching. *)
 
-(* [constr array] is an instance matching definitional [var_context] in
+(* [constr array] is an instance matching definitional [named_context] in
    the same order (i.e. last argument first) *)
 type existential = int * constr array
 type constant = section_path * constr array
@@ -106,6 +91,8 @@ type rec_declaration = constr array * name list * constr array
 type fixpoint = (int array * int) * rec_declaration
 type cofixpoint = int * rec_declaration
 
+(* [IsVar] is used for named variables and [IsRel] for variables as
+   de Bruijn indices. *)
 
 type kind_of_term =
   | IsRel          of int
@@ -178,15 +165,15 @@ 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
+val mkNamedProd_or_LetIn : named_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
+val mkNamedLambda_or_LetIn : named_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
+val mkNamedProd_wo_LetIn : named_declaration -> constr -> constr
 
 (* non-dependant product $t_1 \rightarrow t_2$ *)
 val mkArrow : constr -> constr -> constr
@@ -474,8 +461,8 @@ val substnl : constr list -> int -> constr -> constr
 val substl : constr list -> constr -> constr
 val subst1 : constr -> constr -> constr
 
-val substl_decl : constr list -> var_declaration -> var_declaration
-val subst1_decl : constr -> var_declaration -> var_declaration
+val substl_decl : constr list -> named_declaration -> named_declaration
+val subst1_decl : constr -> named_declaration -> named_declaration
 
 (* [global_vars c] returns the list of [id]'s occurring as [VAR id] in [c] *)
 val global_vars : constr -> identifier list
@@ -525,7 +512,7 @@ val occur_evar : existential_key -> constr -> bool
    in c, [false] otherwise *)
 val occur_var : identifier -> constr -> bool
 
-val occur_var_in_decl : identifier -> var_declaration -> bool
+val occur_var_in_decl : identifier -> named_declaration -> bool
 
 (* [dependent M N] is true iff M is eq\_constr with a subterm of N 
    M is appropriately lifted through abstractions of N *)
@@ -542,7 +529,7 @@ val eta_eq_constr : constr -> constr -> bool
 val subst_term : 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
+      where:named_declaration -> named_declaration
 
 (* [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/typeops.ml b/kernel/typeops.ml
index 31a31a9d90..927b33e8c4 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -52,11 +52,11 @@ let relative env sigma n =
 (* Checks if a context of variable is included in another one. *)
 (*
 let rec hyps_inclusion env sigma sign1 sign2 =
-  if sign1 = empty_var_context then true
+  if sign1 = empty_named_context then true
   else
     let (id1,ty1) = hd_sign sign1 in
     let rec search sign2 =
-      if sign2 = empty_var_context then false
+      if sign2 = empty_named_context then false
       else
 	let (id2,ty2) = hd_sign sign2 in
         if id1 = id2 then
@@ -73,7 +73,7 @@ let rec hyps_inclusion env sigma sign1 sign2 =
    current context of [env]. *)
 (*
 let check_hyps id env sigma hyps =
-  let hyps' = var_context env in
+  let hyps' = named_context env in
   if not (hyps_inclusion env sigma hyps hyps') then
     error_reference_variables CCI env id
 *)
@@ -368,13 +368,13 @@ let check_term env mind_recvec f =
     match lrec, kind_of_term (strip_outer_cast c) with
       | (Param(_)::lr, IsLambda (x,a,b)) -> 
           let l' = map_lift_fst l in
-          crec (push_rel_decl (x,outcast_type a) env) (n+1) l' (lr,b)
+          crec (push_rel_assum (x,outcast_type a) env) (n+1) l' (lr,b)
       | (Norec::lr, IsLambda (x,a,b)) -> 
           let l' = map_lift_fst l in
-          crec (push_rel_decl (x,outcast_type a) env) (n+1) l' (lr,b)
+          crec (push_rel_assum (x,outcast_type a) env) (n+1) l' (lr,b)
       | (Mrec(i)::lr, IsLambda (x,a,b)) -> 
           let l' = map_lift_fst l in
-          crec (push_rel_decl (x,outcast_type a) env) (n+1)
+          crec (push_rel_assum (x,outcast_type a) env) (n+1)
 	    ((1,mind_recvec.(i))::l') (lr,b)
       | (Imbr((sp,i) as ind_sp,lrc)::lr, IsLambda (x,a,b)) -> 
           let l' = map_lift_fst l in
@@ -383,7 +383,7 @@ let check_term env mind_recvec f =
           let lc = 
 	    Array.map (List.map (instantiate_recarg sp lrc)) sprecargs.(i)
 	  in
-          crec (push_rel_decl (x,outcast_type a) env) (n+1) ((1,lc)::l') (lr,b)
+          crec (push_rel_assum (x,outcast_type a) env) (n+1) ((1,lc)::l') (lr,b)
       | _,_ -> f env n l (strip_outer_cast c)
   in 
   crec env
@@ -444,7 +444,7 @@ let is_subterm_specif env sigma lcx mind_recvec =
 	    
       | IsLambda (x,a,b) when l=[] -> 
           let lst' = map_lift_fst lst in
-          crec (push_rel_decl (x,outcast_type a) env) (n+1) lst' b
+          crec (push_rel_assum (x,outcast_type a) env) (n+1) lst' b
 
       (*** Experimental change *************************)
       | IsMeta _ -> [||]
@@ -473,7 +473,7 @@ let rec check_subterm_rec_meta env sigma vectn k def =
      match kind_of_term (strip_outer_cast def) with
        | IsLambda (x,a,b) -> 
 	   if noccur_with_meta n nfi a then
-	     let env' = push_rel_decl (x,outcast_type a) env in
+	     let env' = push_rel_assum (x,outcast_type a) env in
              if n = k+1 then (env',a,b)
 	     else check_occur env' (n+1) b
            else 
@@ -581,13 +581,13 @@ let rec check_subterm_rec_meta env sigma vectn k def =
 
 	| IsLambda (x,a,b) -> 
 	    (check_rec_call env n lst a) &&
-            (check_rec_call (push_rel_decl (x,outcast_type a) env)
+            (check_rec_call (push_rel_assum (x,outcast_type a) env)
 	       (n+1) (map_lift_fst lst) b) &&
             (List.for_all (check_rec_call env n lst) l)
 
 	| IsProd (x,a,b) -> 
 	    (check_rec_call env n lst a) &&
-            (check_rec_call (push_rel_decl (x,outcast_type a) env)
+            (check_rec_call (push_rel_assum (x,outcast_type a) env)
 	       (n+1) (map_lift_fst lst) b) &&
             (List.for_all (check_rec_call env n lst) l)
 
@@ -643,7 +643,7 @@ let rec check_subterm_rec_meta env sigma vectn k def =
 	    | IsLambda (x,a,b) ->
 		(check_rec_call env n lst a) &
 		(check_rec_call_fix_body
-		   (push_rel_decl (x,outcast_type a) env) (n+1)
+		   (push_rel_assum (x,outcast_type a) env) (n+1)
 		   (map_lift_fst lst) (decr-1) recArgsDecrArg b)
 	    | _ -> anomaly "Not enough abstractions in fix body"
     
@@ -683,7 +683,7 @@ let check_guard_rec_meta env sigma nbfix def deftype =
     let b = whd_betadeltaiota env sigma (strip_outer_cast c) in
     match kind_of_term b with
       | IsProd (x,a,b) ->
-	  codomain_is_coind (push_rel_decl (x,outcast_type a) env) b 
+	  codomain_is_coind (push_rel_assum (x,outcast_type a) env) b 
       | _ -> 
 	  try
 	    find_coinductive env sigma b
@@ -756,7 +756,7 @@ let check_guard_rec_meta env sigma nbfix def deftype =
 	| IsLambda (x,a,b) ->
 	     assert (args = []);
             if (noccur_with_meta n nbfix a) then
-              check_rec_call (push_rel_decl (x,outcast_type a) env)
+              check_rec_call (push_rel_assum (x,outcast_type a) env)
 		alreadygrd (n+1)  vlra b
             else 
 	      raise (CoFixGuardError (RecCallInTypeOfAbstraction t))
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index a2fedf7f16..9c4d62b95c 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -51,7 +51,7 @@ val judge_of_prop_contents : contents -> unsafe_judgment
 
 val judge_of_type : universe -> unsafe_judgment * constraints
 
-val generalize_without_universes : var_declaration -> typed_type -> typed_type
+val generalize_without_universes : named_declaration -> typed_type -> typed_type
 
 val abs_rel : 
   env -> 'a evar_map -> name -> typed_type -> unsafe_judgment 
@@ -85,6 +85,6 @@ val find_case_dep_nparams :
   env -> 'a evar_map -> constr * constr -> inductive_family -> constr -> bool
 
 (*i
-val hyps_inclusion : env -> 'a evar_map -> var_context -> var_context -> bool
+val hyps_inclusion : env -> 'a evar_map -> named_context -> named_context -> bool
 i*)