diff options
Diffstat (limited to 'pretyping/typing.ml')
| -rw-r--r-- | pretyping/typing.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml index bd559ddd5..cc473bd86 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_knowing_parameters env (constant_type_in env cst) paramstyp + type_of_constant_type_knowing_parameters env (constant_type_in env cst) paramstyp let inductive_type_knowing_parameters env (ind,u) jl = let mspec = lookup_mind_specif env ind in |