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 }