diff options
Diffstat (limited to 'pretyping/typing.ml')
| -rw-r--r-- | pretyping/typing.ml | 21 |
1 files changed, 13 insertions, 8 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 78902a7d..63fdd6d5 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: typing.ml 8871 2006-05-28 16:46:48Z herbelin $ *) +(* $Id: typing.ml 9310 2006-10-28 19:35:09Z herbelin $ *) open Util open Names @@ -53,7 +53,7 @@ let rec execute env evd cstr = j_nf_evar (evars_of evd) (judge_of_variable env id) | Const c -> - make_judge cstr (nf_evar (evars_of evd) (constant_type env c)) + make_judge cstr (nf_evar (evars_of evd) (type_of_constant env c)) | Ind ind -> make_judge cstr (nf_evar (evars_of evd) (type_of_inductive env ind)) @@ -90,12 +90,17 @@ let rec execute env evd cstr = | App (f,args) -> let jl = execute_array env evd args in let j = - if isInd f then - (* Sort-polymorphism of inductive types *) - judge_of_inductive_knowing_parameters env (destInd f) - (jv_nf_evar (evars_of evd) jl) - else - execute env evd f + match kind_of_term f with + | Ind ind -> + (* Sort-polymorphism of inductive types *) + judge_of_inductive_knowing_parameters env ind + (jv_nf_evar (evars_of evd) jl) + | Const cst -> + (* Sort-polymorphism of inductive types *) + judge_of_constant_knowing_parameters env cst + (jv_nf_evar (evars_of evd) jl) + | _ -> + execute env evd f in fst (judge_of_apply env j jl) |