diff options
Diffstat (limited to 'pretyping/typing.ml')
| -rw-r--r-- | pretyping/typing.ml | 31 |
1 files changed, 19 insertions, 12 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml index a15134f58d..f067c075bf 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -27,6 +27,8 @@ open Arguments_renaming open Pretype_errors open Context.Rel.Declaration +module GR = Names.GlobRef + let meta_type evd mv = let ty = try Evd.meta_ftype evd mv @@ -36,8 +38,11 @@ let meta_type evd mv = let inductive_type_knowing_parameters env sigma (ind,u) jl = let u = Unsafe.to_instance u in let mspec = lookup_mind_specif env ind in - let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr ~abort_on_undefined_evars:false sigma j.uj_type)) jl in - Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp + let paramstyp = Array.map_to_list (fun j () -> + let s = Reductionops.sort_of_arity env sigma j.uj_type in + Sorts.univ_of_sort (EConstr.ESorts.kind sigma s)) jl + in + Inductive.type_of_inductive_knowing_parameters (mspec,u) paramstyp let type_judgment env sigma j = match EConstr.kind sigma (whd_all env sigma j.uj_type) with @@ -253,6 +258,9 @@ let judge_of_type u = let judge_of_relative env v = Environ.on_judgment EConstr.of_constr (judge_of_relative env v) +let type_of_variable env id = + EConstr.of_constr (type_of_variable env id) + let judge_of_variable env id = Environ.on_judgment EConstr.of_constr (judge_of_variable env id) @@ -284,37 +292,36 @@ let judge_of_letin env name defj typj j = { uj_val = mkLetIn (make_annot name r, defj.uj_val, typj.utj_val, j.uj_val) ; uj_type = subst1 defj.uj_val j.uj_type } -let check_hyps_inclusion env sigma f x hyps = +let check_hyps_inclusion env sigma x hyps = let evars = Evarutil.safe_evar_value sigma, Evd.universes sigma in - let f x = EConstr.Unsafe.to_constr (f x) in - Typeops.check_hyps_inclusion env ~evars f x hyps + Typeops.check_hyps_inclusion env ~evars x hyps let type_of_constant env sigma (c,u) = let open Declarations in let cb = Environ.lookup_constant c env in - let () = check_hyps_inclusion env sigma mkConstU (c,u) cb.const_hyps in + let () = check_hyps_inclusion env sigma (GR.ConstRef c) cb.const_hyps in let u = EInstance.kind sigma u in let ty, csts = Environ.constant_type env (c,u) in let sigma = Evd.add_constraints sigma csts in - sigma, (EConstr.of_constr (rename_type ty (Names.GlobRef.ConstRef c))) + sigma, (EConstr.of_constr (rename_type ty (GR.ConstRef c))) let type_of_inductive env sigma (ind,u) = let open Declarations in let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in - let () = check_hyps_inclusion env sigma mkIndU (ind,u) mib.mind_hyps in + let () = check_hyps_inclusion env sigma (GR.IndRef ind) mib.mind_hyps in let u = EInstance.kind sigma u in - let ty, csts = Inductive.constrained_type_of_inductive env (specif,u) in + let ty, csts = Inductive.constrained_type_of_inductive (specif,u) in let sigma = Evd.add_constraints sigma csts in - sigma, (EConstr.of_constr (rename_type ty (Names.GlobRef.IndRef ind))) + sigma, (EConstr.of_constr (rename_type ty (GR.IndRef ind))) let type_of_constructor env sigma ((ind,_ as ctor),u) = let open Declarations in let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in - let () = check_hyps_inclusion env sigma mkIndU (ind,u) mib.mind_hyps in + let () = check_hyps_inclusion env sigma (GR.IndRef ind) mib.mind_hyps in let u = EInstance.kind sigma u in let ty, csts = Inductive.constrained_type_of_constructor (ctor,u) specif in let sigma = Evd.add_constraints sigma csts in - sigma, (EConstr.of_constr (rename_type ty (Names.GlobRef.ConstructRef ctor))) + sigma, (EConstr.of_constr (rename_type ty (GR.ConstructRef ctor))) let judge_of_int env v = Environ.on_judgment EConstr.of_constr (judge_of_int env v) |