diff options
| author | filliatr | 1999-12-01 08:03:06 +0000 |
|---|---|---|
| committer | filliatr | 1999-12-01 08:03:06 +0000 |
| commit | dda7c7bb0b6ea0c2106459d8ae208eff0dfd6738 (patch) | |
| tree | 21bd3b1535e2e9b9cfcfa0f8cab47817a1769b70 /parsing | |
| parent | 8b882c1ab5a31eea35eec89f134238dd17b945c2 (diff) | |
- 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
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/astterm.ml | 5 | ||||
| -rw-r--r-- | parsing/pretty.ml | 6 |
2 files changed, 5 insertions, 6 deletions
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 -> |