diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/pretyping.ml | 2 | ||||
| -rw-r--r-- | pretyping/retyping.ml | 3 | ||||
| -rw-r--r-- | pretyping/typing.ml | 2 |
3 files changed, 3 insertions, 4 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 6d7403031a..c8c1d0e213 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -311,7 +311,7 @@ let pretype_ref loc evdref env ref us = | ref -> let evd, c = pretype_global loc univ_flexible env !evdref ref us in let () = evdref := evd in - let ty = Retyping.get_type_of env evd c in + let ty = Typing.type_of env evd c in make_judge c ty let judge_of_Type evd s = diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index aa33c32863..c7bdabe93f 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -183,8 +183,7 @@ let retype ?(polyprop=true) sigma = ~polyprop env (mip,snd ind) argtyps with Reduction.NotArity -> retype_error NotAnArity) | Const cst -> - let t = constant_type_in env cst in - (try Typeops.type_of_constant_type_knowing_parameters env t argtyps + (try Typeops.type_of_constant_knowing_parameters_in env cst argtyps with Reduction.NotArity -> retype_error NotAnArity) | Var id -> type_of_var env id | Construct cstr -> type_of_constructor env cstr diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 92bdd35ecf..669fbfb46e 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -27,7 +27,7 @@ let meta_type evd mv = let constant_type_knowing_parameters env cst jl = let paramstyp = Array.map (fun j -> lazy j.uj_type) jl in - type_of_constant_type_knowing_parameters env (constant_type_in env cst) paramstyp + type_of_constant_knowing_parameters_in env cst paramstyp let inductive_type_knowing_parameters env (ind,u) jl = let mspec = lookup_mind_specif env ind in |