- Typing -> Safe_typing

 - proofs/Typing_ev -> pretyping/Typing
 - env -> sign
 - fonctions var_context


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

10 files changed, 41 insertions, 37 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index ccf3e1e20c..bed45797d8 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -43,6 +43,7 @@ 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
 
 (* Construction functions. *)
 
@@ -50,8 +51,8 @@ let push_var idvar env =
   { env with env_context = add_glob idvar env.env_context }
 
 let change_hyps f env =
-  let ctx = env.env_context in
-  { env with env_context = ENVIRON (f (get_globals ctx), get_rels ctx) }
+  let (ENVIRON(g,r)) = env.env_context in
+  { env with env_context = ENVIRON (f g, r) }
 
 let push_rel idrel env =
   { env with env_context = add_rel idrel env.env_context }
diff --git a/kernel/environ.mli b/kernel/environ.mli
index d3fd22c01e..9f1c228a00 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -22,6 +22,7 @@ val empty_env : unsafe_env
 
 val universes : unsafe_env -> universes
 val context : unsafe_env -> context
+val var_context : unsafe_env -> var_context
 
 val push_var : identifier * typed_type -> unsafe_env -> unsafe_env
 val change_hyps : 
diff --git a/kernel/evd.ml b/kernel/evd.ml
index dd387ddfb4..4599fbdc43 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 = get_globals (context ev.evar_env)
+let evar_hyps ev = var_context ev.evar_env
 
 let id_of_existential ev =
   id_of_string ("?" ^ string_of_int ev)
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 96fe8d5846..00e8a442bb 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -244,7 +244,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 = get_globals (context env);
+    mind_hyps = var_context env;
     mind_packets = packets;
     mind_constraints = cst;
     mind_singl = None;
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 4bc551c6aa..2ce121ed12 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -1296,17 +1296,17 @@ let nf_ise1 sigma = strong (fun _ -> whd_ise1) empty_env sigma
 (* Same as whd_ise1, but replaces the remaining ISEVAR by Metavariables
  * Similarly we have is_fmachine1_metas and is_resolve1_metas *)
 
-let rec whd_ise1_metas env sigma = function
+let rec whd_ise1_metas sigma = function
   | (DOPN(Evar n,_) as k) ->
       if Evd.in_dom sigma n then
 	if Evd.is_defined sigma n then
-      	  whd_ise1_metas env sigma (existential_value sigma k)
+      	  whd_ise1_metas sigma (existential_value sigma k)
 	else 
       	  let m = DOP0(Meta (new_meta())) in
 	  DOP2(Cast,m,existential_type sigma k)
       else
 	k
-  | DOP2(Cast,c,_) -> whd_ise1_metas env sigma c
+  | DOP2(Cast,c,_) -> whd_ise1_metas sigma c
   | c -> c
 
 
diff --git a/kernel/typing.ml b/kernel/safe_typing.ml
index db3d00302e..e523be5108 100644
--- a/kernel/typing.ml
+++ b/kernel/safe_typing.ml
@@ -233,6 +233,7 @@ let empty_environment = empty_env
 
 let universes = universes
 let context = context
+let var_context = var_context
 
 let lookup_var = lookup_var
 let lookup_rel = lookup_rel
@@ -283,7 +284,7 @@ let add_constant sp ce env =
     const_kind = kind_of_path sp;
     const_body = Some ce.const_entry_body;
     const_type = ty;
-    const_hyps = get_globals (context env);
+    const_hyps = var_context env;
     const_constraints = Constraint.union cst cst';
     const_opaque = false } 
   in
@@ -296,7 +297,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 = get_globals (context env);
+    const_hyps = var_context env;
     const_constraints = cst;
     const_opaque = false } 
   in
diff --git a/kernel/typing.mli b/kernel/safe_typing.mli
index 10530d123b..392040814f 100644
--- a/kernel/typing.mli
+++ b/kernel/safe_typing.mli
@@ -24,6 +24,7 @@ val empty_environment : environment
 
 val universes : environment -> universes
 val context : environment -> context
+val var_context : environment -> var_context
 
 val push_var : identifier * constr -> environment -> environment
 val push_rel : name * constr -> environment -> environment
diff --git a/kernel/sign.ml b/kernel/sign.ml
index 5d7d5309b0..0b34c7edf3 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -10,7 +10,7 @@ open Term
 
 type 'a signature = identifier list * 'a list
 type 'a db_signature = (name * 'a) list
-type ('a,'b) env = ENVIRON of 'a signature * 'b db_signature
+type ('a,'b) sign = ENVIRON of 'a signature * 'b db_signature
 
 let gLOB hyps = ENVIRON (hyps,[])
 
@@ -233,7 +233,7 @@ let lookup_id id env =
     | Not_found -> let (x,y) = lookup_glob id env in GLOBNAME(x,y)
 
 
-type 'b assumptions = (typed_type,'b) env
-type context = (typed_type,typed_type) env
+type 'b assumptions = (typed_type,'b) sign
+type context = (typed_type,typed_type) sign
 type var_context = typed_type signature
 
diff --git a/kernel/sign.mli b/kernel/sign.mli
index 2a0a567dec..e2ef7d4a1e 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -54,35 +54,35 @@ val dbindv : 'a signature -> 'b term array -> 'a * 'b term
 (*s Signatures with named and de Bruijn variables. *)
 
 type 'a db_signature = (name * 'a) list
-type ('a,'b) env = ENVIRON of 'a signature * 'b db_signature
-
-val gLOB : 'b signature -> ('b,'a) env
-
-val add_rel : (name * 'a) -> ('b,'a) env -> ('b,'a) env 
-val add_glob : (identifier * 'b) -> ('b,'a) env -> ('b,'a) env
-val lookup_glob : identifier -> ('b,'a) env -> (identifier * 'b)
-val lookup_rel : int -> ('b,'a) env  -> (name * 'a)
-val mem_glob : identifier -> ('b,'a) env -> bool
-
-val get_globals : ('b,'a) env -> 'b signature
-val get_rels : ('b,'a) env -> 'a db_signature
-val dbenv_it : (name -> 'b -> 'c -> 'c) -> ('a,'b) env -> 'c -> 'c
-val it_dbenv : ('c -> name -> 'b -> 'c) -> 'c -> ('a,'b) env -> 'c
-val map_rel_env : ('a -> 'b) -> ('c,'a) env -> ('c,'b) env
-val map_var_env : ('c -> 'b) -> ('c,'a) env -> ('b,'a) env
-val isnull_rel_env : ('a,'b) env -> bool
-val uncons_rel_env : ('a,'b) env -> (name * 'b) * ('a,'b) env
-val ids_of_env : ('a, 'b) env -> identifier list
+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 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
 
 type ('b,'a) search_result =
   | GLOBNAME of identifier  * 'b
   | RELNAME of int * 'a
 
-val lookup_id : identifier -> ('b,'a) env -> ('b,'a) search_result
+val lookup_id : identifier -> ('b,'a) sign -> ('b,'a) search_result
 
 
-type 'b assumptions = (typed_type,'b) env
-type context = (typed_type,typed_type) env
+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
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index d224b0209e..0d2d5cba50 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -75,14 +75,14 @@ let hyps_inclusion env sigma (idl1,tyl1) (idl2,tyl2) =
    current context of [env]. *)
 
 let construct_reference id env sigma hyps =
-  let hyps' = get_globals (context env) in
+  let hyps' = var_context env in
   if hyps_inclusion env sigma hyps hyps' then
     Array.of_list (List.map (fun id -> VAR id) (ids_of_sign hyps))
   else 
     error_reference_variables CCI env id
 
 let check_hyps id env sigma hyps =
-  let hyps' = get_globals (context env) in
+  let hyps' = var_context env in
   if not (hyps_inclusion env sigma hyps hyps') then
     error_reference_variables CCI env id
 
@@ -178,7 +178,7 @@ let type_inst_construct env sigma i mind =
 let type_of_existential env sigma c =
   let (ev,args) = destEvar c in
   let evi = Evd.map sigma ev in
-  let hyps = get_globals (context evi.Evd.evar_env) in
+  let hyps = var_context evi.Evd.evar_env in
   let id = id_of_string ("?" ^ string_of_int ev) in
   check_hyps id env sigma hyps;
   instantiate_constr (ids_of_sign hyps) evi.Evd.evar_concl (Array.to_list args)