diff options
| author | Pierre-Marie Pédrot | 2020-02-14 23:48:57 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-02-14 23:48:57 +0100 |
| commit | 4de476c53d85be4dd266cfe5fd5f2ddec9163a5b (patch) | |
| tree | 1f8cb4ea4350ee9dfef0d65a90aebdd3d939c1d5 /pretyping/typing.ml | |
| parent | bdc8e29d806ab7e9bbd0491bf237890b7934795a (diff) | |
| parent | 0f58738351db02f30ac43ec52517c54b315d5886 (diff) | |
Merge PR #11557: Use thunks to univ instead of lazy constr for template typing
Reviewed-by: ppedrot
Diffstat (limited to 'pretyping/typing.ml')
| -rw-r--r-- | pretyping/typing.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml index b4c19775a7..f067c075bf 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -38,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 @@ -307,7 +310,7 @@ let type_of_inductive env sigma (ind,u) = let (mib,_ as specif) = Inductive.lookup_mind_specif env ind 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 (GR.IndRef ind))) |