diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-05-14 18:38:14 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-05-14 18:38:14 +0000 |
commit | fd7448ad0f44ef306d910816d7b6d2f6a303f4a7 (patch) | |
tree | 5a5c51c01bbbaa75a4ddffcca384cdf5cc7d0d2e /kernel/typeops.ml | |
parent | 23a51bab686dd0ceaa9a87b09beb49d0ee0575c4 (diff) |
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
Diffstat (limited to 'kernel/typeops.ml')
-rw-r--r-- | kernel/typeops.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index cc7cf0c68..a9cc151cf 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -152,7 +152,7 @@ let judge_of_constant_knowing_parameters env cst jl = let c = mkConst cst in let cb = lookup_constant cst env in let _ = check_hyps_inclusion env c cb.const_hyps in - let paramstyp = Array.map (fun j -> j.uj_type) jl in + let paramstyp = Array.map (fun j -> lazy j.uj_type) jl in let t = type_of_constant_knowing_parameters env cb.const_type paramstyp in make_judge c t @@ -298,7 +298,7 @@ let judge_of_inductive_knowing_parameters env ind jl = let c = mkInd ind in let (mib,mip) = lookup_mind_specif env ind in check_hyps_inclusion env c mib.mind_hyps; - let paramstyp = Array.map (fun j -> j.uj_type) jl in + let paramstyp = Array.map (fun j -> lazy j.uj_type) jl in let t = Inductive.type_of_inductive_knowing_parameters env mip paramstyp in make_judge c t |