From dda7c7bb0b6ea0c2106459d8ae208eff0dfd6738 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Wed, 1 Dec 1999 08:03:06 +0000
Subject:  - 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
---
 kernel/typeops.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'kernel/typeops.ml')

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)
-- 
cgit v1.2.3