diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-12-01 08:03:06 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-12-01 08:03:06 +0000 |
| commit | dda7c7bb0b6ea0c2106459d8ae208eff0dfd6738 (patch) | |
| tree | 21bd3b1535e2e9b9cfcfa0f8cab47817a1769b70 /parsing/pretty.ml | |
| 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/pretty.ml')
| -rw-r--r-- | parsing/pretty.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/parsing/pretty.ml b/parsing/pretty.ml index 058844622..ea83e68b1 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 -> |