- 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

1 files changed, 3 insertions, 2 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 }