From fd7448ad0f44ef306d910816d7b6d2f6a303f4a7 Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 14 May 2013 18:38:14 +0000 Subject: Delayed the computation of parameters in sort polymorphism of inductive types. This saves some computation, but also allows incidentally to retype terms with evars without failing if an inductive type as an argument whose type is an evar. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16526 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/typing.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'pretyping/typing.ml') diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 008b8b9a3..9fe95a119 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -27,12 +27,12 @@ let meta_type evd mv = meta_instance evd ty let constant_type_knowing_parameters env cst jl = - let paramstyp = Array.map (fun j -> j.uj_type) jl in + let paramstyp = Array.map (fun j -> lazy j.uj_type) jl in type_of_constant_knowing_parameters env (constant_type env cst) paramstyp let inductive_type_knowing_parameters env ind jl = let (mib,mip) = lookup_mind_specif env ind in - let paramstyp = Array.map (fun j -> j.uj_type) jl in + let paramstyp = Array.map (fun j -> lazy j.uj_type) jl in Inductive.type_of_inductive_knowing_parameters env mip paramstyp let e_type_judgment env evdref j = -- cgit v1.2.3