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

9 files changed, 36 insertions, 36 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 9d536b644a..176a3c3e9e 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -136,7 +136,7 @@ let inductive_of_rawconstructor c =
 
 (* Environment management *)
 let push_rel_type sigma (na,t) env =
-  push_rel_decl (na,get_assumption_of env sigma t) env
+  push_rel_assum (na,get_assumption_of env sigma t) env
 
 let push_rels vars env =
   List.fold_right (fun nvar env -> push_rel_type Evd.empty nvar env) vars env
@@ -750,7 +750,7 @@ let shift_problem pb =
 
 (* Building the sub-pattern-matching problem for a given branch *)
 let build_branch pb defaults eqns const_info =
-  let cs_args = decls_of_rel_context const_info.cs_args in
+  let cs_args = assums_of_rel_context const_info.cs_args in
   let names = get_names pb.env cs_args eqns in
   let newpats =
     if !substitute_alias then
@@ -764,7 +764,7 @@ let build_branch pb defaults eqns const_info =
   let _,typs' =
     List.fold_right
       (fun (na,t) (env,typs) ->
- 	 (push_rel_decl (na,outcast_type t) env,
+ 	 (push_rel_assum (na,outcast_type t) env,
 	  ((na,to_mutind env !(pb.isevars) t),t)::typs))
       typs (pb.env,[]) in
   let tomatchs =
@@ -882,7 +882,7 @@ let matx_of_eqns env tomatchl eqns =
     let initial_lpat,initial_rhs = prepare_initial_alias lpat tomatchl rhs in
     let rhs =
       { rhs_env = env;
-	other_ids = ids@(ids_of_var_context (var_context env));
+	other_ids = ids@(ids_of_named_context (named_context env));
 	private_ids = [];
 	user_ids = ids;
 	subst = [];
@@ -924,7 +924,7 @@ let inh_coerce_to_ind isevars env ty tyi =
     List.fold_right
       (fun (na,ty) (env,evl) ->
 	 let aty = get_assumption_of env Evd.empty ty in
-	   (push_rel_decl (na,aty) env,
+	   (push_rel_assum (na,aty) env,
 	    (new_isevar isevars env (incast_type aty) CCI)::evl))
       ntys (env,[]) in
   let expected_typ = applist (mkMutInd tyi,evarl) in
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 839cfac4f1..9040ce3eb3 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -131,7 +131,7 @@ let rec inh_conv_coerce_to_fail env isevars c1 hj =
                (* let jv1 = exemeta_rec def_vty_con env isevars v1 in 
 	          let assv1 = assumption_of_judgement env !isevars jv1 in *)
 	       let assv1 = outcast_type v1 in
-               let env1 = push_rel_decl (x,assv1) env in
+               let env1 = push_rel_assum (x,assv1) env in
                let h2 = inh_conv_coerce_to_fail env isevars u2
 			  {uj_val = v2;
 			   uj_type = get_assumption_of env1 !isevars t2 } in
@@ -141,7 +141,7 @@ let rec inh_conv_coerce_to_fail env isevars c1 hj =
                let name = (match name with 
 			     | Anonymous -> Name (id_of_string "x")
                              | _ -> name) in
-               let env1 = push_rel_decl (name,assu1) env in
+               let env1 = push_rel_assum (name,assu1) env in
                let h1 = 
 		 inh_conv_coerce_to_fail env isevars t1
 		   {uj_val = mkRel 1; 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index a49bcb098f..70eba2949e 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -253,7 +253,7 @@ let lookup_name_as_renamed ctxt t s =
 	   | (None,avoid')    -> lookup avoid' env_names (n+1) (pop c'))
     | IsCast (c,_) -> lookup avoid env_names n c
     | _ -> None
-  in lookup (ids_of_var_context ctxt) empty_names_context 1 t
+  in lookup (ids_of_named_context ctxt) empty_names_context 1 t
 
 let lookup_index_as_renamed t n =
   let rec lookup n d c = match kind_of_term c with
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 8c8dd417d1..5f3108d483 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -15,7 +15,7 @@ open Rawterm
 val detype : identifier list -> names_context -> constr -> rawconstr
 
 (* look for the index of a named var or a nondep var as it is renamed *)
-val lookup_name_as_renamed : var_context -> constr -> identifier -> int option
+val lookup_name_as_renamed : named_context -> constr -> identifier -> int option
 val lookup_index_as_renamed : constr -> int -> int option
 
 
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index b877624ada..f4e9d01b7a 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -264,7 +264,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
         evar_conv_x env isevars CONV c1 c2
         & 
 	(let d = Retyping.get_assumption_of env !isevars (nf_ise1 !isevars c1)
-	 in evar_conv_x (push_rel_decl (n,d) env) isevars pbty c'1 c'2)
+	 in evar_conv_x (push_rel_assum (n,d) env) isevars pbty c'1 c'2)
 
     | IsMutInd (sp1,cl1), IsMutInd (sp2,cl2) ->
 	sp1=sp2
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index b7061962bf..8aac75e39f 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -45,8 +45,8 @@ let filter_sign p sign x =
 
 (* All ids of sign must be distincts! *)
 let new_isevar_sign env sigma typ instance =
-  let sign = var_context env in
-  if not (list_distinct (ids_of_var_context sign)) then 
+  let sign = named_context env in
+  if not (list_distinct (ids_of_named_context sign)) then 
     error "new_isevar_sign: two vars have the same name";
   let newev = Evd.new_evar() in
   let info = { evar_concl = typ; evar_env = env; 
@@ -58,7 +58,7 @@ let new_isevar_sign env sigma typ instance =
 let dummy_sort = mkType dummy_univ
 
 let make_instance env =
-  fold_var_context
+  fold_named_context
     (fun env (id, b, _) l -> if b=None then mkVar id :: l else l)
     env []
 
@@ -74,9 +74,9 @@ let split_evar_to_arrow sigma c =
   let evd = Evd.map sigma ev in
   let evenv = evd.evar_env in
   let (sigma1,dom) = new_type_var evenv sigma in
-  let hyps = var_context evenv in
-  let nvar = next_ident_away (id_of_string "x") (ids_of_var_context hyps) in
-  let newenv = push_var_decl (nvar,make_typed dom (Type dummy_univ)) evenv in
+  let hyps = named_context evenv in
+  let nvar = next_ident_away (id_of_string "x") (ids_of_named_context hyps) in
+  let newenv = push_named_assum (nvar,make_typed dom (Type dummy_univ)) evenv in
   let (sigma2,rng) = new_type_var newenv sigma1 in
   let prod = mkProd (named_hd newenv dom Anonymous, dom, subst_var nvar rng) in
   let sigma3 = Evd.define sigma2 ev prod in
@@ -100,7 +100,7 @@ let do_restrict_hyps sigma c =
   let args = Array.to_list args in
   let evd = Evd.map sigma ev in
   let env = evd.evar_env in
-  let hyps = var_context env in
+  let hyps = named_context env in
   let (_,(rsign,ncargs)) =
     List.fold_left 
       (fun (sign,(rs,na)) a ->
@@ -108,7 +108,7 @@ let do_restrict_hyps sigma c =
 	  if not(closed0 a) then 
 	    (rs,na)
 	  else 
-	    (add_var (List.hd sign) rs, a::na)))
+	    (add_named_decl (List.hd sign) rs, a::na)))
       (hyps,([],[])) args 
   in
   let sign' = List.rev rsign in
@@ -146,7 +146,7 @@ let ise_try isevars l =
 (* say if the section path sp corresponds to an existential *)
 let ise_in_dom isevars sp = Evd.in_dom !isevars sp
 
-(* map the given section path to the evar_declaration *)
+(* map the given section path to the enamed_declaration *)
 let ise_map isevars sp = Evd.map !isevars sp
 
 (* define the existential of section path sp as the constr body *)
@@ -198,7 +198,7 @@ let real_clean isevars sp args rhs =
 let make_instance_with_rel env =
   let n = rel_context_length (rel_context env) in
   let vars = 
-    fold_var_context
+    fold_named_context
       (fun env (id,b,_) l -> if b=None then mkVar id :: l else l)
       env [] in
   snd (fold_rel_context
@@ -206,7 +206,7 @@ let make_instance_with_rel env =
     env (n+1,vars))
 
 let make_subst env args =
-  snd (fold_var_context
+  snd (fold_named_context
     (fun env (id,b,c) (args,l as g) ->
        match b, args with
 	 | None, a::rest -> (rest, (id,a)::l)
@@ -218,7 +218,7 @@ let make_subst env args =
 (* Converting the env into the sign of the evar to define *)
 
 let new_isevar isevars env typ k =
-  let subst,env' = push_rels_to_vars env in
+  let subst,env' = push_rel_context_to_named_context env in
   let typ' = substl subst typ in
   let instance = make_instance_with_rel env in
   let (sigma',evar) = new_isevar_sign env' !isevars typ' instance in
@@ -270,19 +270,19 @@ let solve_refl conv_algo isevars c1 c2 =
   and (_,argsv2) = destEvar c2 in
   let evd = Evd.map !isevars ev in
   let env = evd.evar_env in
-  let hyps = var_context env in
+  let hyps = named_context env in
   let (_,rsign) = 
     array_fold_left2
       (fun (sgn,rsgn) a1 a2 ->
 	 if conv_algo a1 a2 then 
-	   (List.tl sgn, add_var (List.hd sgn) rsgn)
+	   (List.tl sgn, add_named_decl (List.hd sgn) rsgn)
 	 else 
 	   (List.tl  sgn, rsgn))
       (hyps,[]) argsv1 argsv2 
   in
   let nsign = List.rev rsign in
   let nenv = change_hyps (fun _ -> nsign) env in
-  let nargs = (Array.of_list (List.map mkVar (ids_of_var_context nsign))) in
+  let nargs = (Array.of_list (List.map mkVar (ids_of_named_context nsign))) in
   let newev = Evd.new_evar () in
   let info = { evar_concl = evd.evar_concl; evar_env = nenv;
 	       evar_body = Evar_empty; evar_info = None } in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index a7ac436b60..9caab6bcce 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -159,7 +159,7 @@ let pretype_id loc env lvar id =
     { uj_val  = mkRel n; uj_type = typed_app (lift n) typ }
   with Not_found ->
   try
-    let typ = lookup_id_type id (var_context env) in
+    let typ = lookup_id_type id (named_context env) in
     { uj_val  = mkVar id; uj_type = typ }
   with Not_found ->
     error_var_not_found_loc loc CCI id
@@ -240,7 +240,7 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
   let nbfix = Array.length lfi in
   let lfi = List.map (fun id -> Name id) (Array.to_list lfi) in
   let newenv =
-    array_fold_left2 (fun env id ar -> (push_rel_decl (id,ar) env))
+    array_fold_left2 (fun env id ar -> (push_rel_assum (id,ar) env))
       env (Array.of_list (List.rev lfi)) (vect_lift_type lara) in
   let vdefj =
     Array.mapi 
@@ -280,7 +280,7 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
     let j = pretype_type dom_valcon env isevars lvar lmeta c1 in
     let assum = assumption_of_type_judgment (inh_ass_of_j env isevars j) in
     let var = (name,assum) in
-    let j' = pretype rng (push_rel_decl var env) isevars lvar lmeta c2 
+    let j' = pretype rng (push_rel_assum var env) isevars lvar lmeta c2 
     in 
     fst (abs_rel env !isevars name assum j')
 
@@ -288,7 +288,7 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
     let j = pretype empty_tycon env isevars lvar lmeta c1 in
     let assum = inh_ass_of_j env isevars j in
     let var = (name,assumption_of_type_judgment assum) in
-    let j' = pretype empty_tycon (push_rel_decl var env) isevars lvar lmeta c2 in
+    let j' = pretype empty_tycon (push_rel_assum var env) isevars lvar lmeta c2 in
     (try fst (gen_rel env !isevars name assum j')
      with TypeError _ as e -> Stdpp.raise_with_loc loc e)
 
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 1e7da45794..4f36fbbdd0 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -45,7 +45,7 @@ let rec type_of env cstr=
            with Not_found -> anomaly "type_of: this is not a well-typed term")
     | IsRel n -> lift n (body_of_type (snd (lookup_rel_type n env)))
     | IsVar id ->
-      (try body_of_type (snd (lookup_var id env))
+      (try body_of_type (snd (lookup_named id env))
        with Not_found ->
          anomaly ("type_of: variable "^(string_of_id id)^" unbound"))
     | IsConst c -> body_of_type (type_of_constant env sigma c)
@@ -64,7 +64,7 @@ let rec type_of env cstr=
         whd_betadeltaiota env sigma (applist (p,al))
     | IsLambda (name,c1,c2) ->
         let var = make_typed c1 (sort_of env c1) in
-          mkProd (name, c1, type_of (push_rel_decl (name,var) env) c2)
+          mkProd (name, c1, type_of (push_rel_assum (name,var) env) c2)
     | IsLetIn (name,b,c1,c2) ->
         let var = make_typed c1 (sort_of env c1) in
          subst1 b (type_of (push_rel_def (name,b,var) env) c2)
@@ -84,7 +84,7 @@ and sort_of env t =
     | IsSort (Type u) -> Type Univ.dummy_univ
     | IsProd (name,t,c2) ->
         let var = make_typed t (sort_of env t) in
-        (match (sort_of (push_rel_decl (name,var) env) c2) with
+        (match (sort_of (push_rel_assum (name,var) env) c2) with
 	  | Prop _ as s -> s
 	  | Type u2 -> Type Univ.dummy_univ)
     | IsApp(f,args) -> sort_of_atomic_type env sigma (type_of env f) args
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 8b9319a29c..ebab35c2cd 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -36,7 +36,7 @@ let rec execute mf env sigma cstr =
 
     | IsVar id -> 
       (try
-         make_judge cstr (snd (lookup_var id env))
+         make_judge cstr (snd (lookup_named id env))
        with Not_found ->
          error ("execute: variable " ^ (string_of_id id) ^ " not defined"))
 	  
@@ -86,7 +86,7 @@ let rec execute mf env sigma cstr =
     | IsLambda (name,c1,c2) -> 
         let j = execute mf env sigma c1 in
 	let var = assumption_of_judgment env sigma j in
-	let env1 = push_rel_decl (name,var) env in
+	let env1 = push_rel_assum (name,var) env in
         let j' = execute mf env1 sigma c2 in 
         let (j,_) = abs_rel env1 sigma name var j' in
 	j
@@ -95,7 +95,7 @@ let rec execute mf env sigma cstr =
         let j = execute mf env sigma c1 in
         let varj = type_judgment env sigma j in
 	let var = assumption_of_type_judgment varj in
-	let env1 = push_rel_decl (name,var) env in
+	let env1 = push_rel_assum (name,var) env in
         let j' = execute mf env1 sigma c2 in
 	let (j,_) = gen_rel env1 sigma name varj j' in
 	j
@@ -121,7 +121,7 @@ and execute_fix mf env sigma 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 = execute_array mf env1 sigma vdef in
   let vdefv = Array.map j_val_only vdefj in
   let cst3 = type_fixpoint env1 sigma lfi lara vdefj in