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
---
 parsing/astterm.ml | 5 ++---
 parsing/pretty.ml  | 6 +++---
 2 files changed, 5 insertions(+), 6 deletions(-)

(limited to 'parsing')

diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index fddb478045..f2befc1d26 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -615,7 +615,7 @@ let ast_adjust_consts sigma = (* locations are kept *)
 
 let globalize_command ast =
   let env = Global.unsafe_env () in
-  let sign = get_globals (Environ.context env) in
+  let sign = Environ.var_context env in
   ast_adjust_consts Evd.empty (gLOB sign) ast
 
 (* Avoid globalizing in non command ast for tactics *)
@@ -633,8 +633,7 @@ let rec glob_ast sigma env = function
   | x -> x
 
 let globalize_ast ast =
-  let env = Global.unsafe_env () in
-  let sign = get_globals (Environ.context env) in
+  let sign = Global.var_context () in
   glob_ast Evd.empty (gLOB sign) ast
 
 
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 0588446225..ea83e68b1f 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -42,7 +42,7 @@ let print_basename_mind sp mindid =
 let print_closed_sections = ref false
 
 let print_typed_value_in_env env (trm,typ) =
-  let sign = get_globals (Environ.context env) in
+  let sign = Environ.var_context env in
   [< term0 (gLOB sign) trm ; 'fNL ;
      'sTR "     : "; term0 (gLOB sign) typ ; 'fNL >]
 
@@ -352,7 +352,7 @@ let print_constructors_rel fn mip =
   List.iter (function (id,c) -> fn (string_of_id id) ass_name c) flid
 
 let crible (fn:string -> unit assumptions -> constr -> unit) name =
-  let hyps = gLOB (get_globals (Global.context())) in
+  let hyps = gLOB (Global.var_context()) in
   let imported = Library.opened_modules() in
   let const = global_reference CCI name in 
   let rec crible_rec = function
@@ -438,7 +438,7 @@ let print_name name =
 let print_opaque_name name = 
   let sigma = Evd.empty in
   let env = Global.unsafe_env () in
-  let sign = get_globals (Global.context ()) in
+  let sign = Global.var_context () in
   try 
     match global_reference CCI name with
       | DOPN(Const sp,_) as x ->
-- 
cgit v1.2.3