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 /proofs/clenv.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 'proofs/clenv.ml')
| -rw-r--r-- | proofs/clenv.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 4c14040bdd..80aae11823 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -33,7 +33,7 @@ type 'a clausenv = { type wc = walking_constraints let new_evar_in_sign env = - let hyps = get_globals (Environ.context env) in + let hyps = Environ.var_context env in let ev = new_evar () in DOPN(Evar ev, Array.of_list (List.map (fun id -> VAR id) (ids_of_sign hyps))) @@ -881,10 +881,10 @@ let clenv_type_of ce c = | (n,Cltyp typ) -> (n,typ.rebus)) (intmap_to_list ce.env) in - failwith "TODO: clenv_type_of" + failwith "TODO" (*** - (Trad.ise_resolve true (w_Underlying ce.hook) metamap - (gLOB(w_hyps ce.hook)) c)._TYPE + (Pretyping.ise_resolve true (w_Underlying ce.hook) metamap + (gLOB(w_hyps ce.hook)) c).uj_type ***) let clenv_instance_type_of ce c = |