diff options
| author | herbelin | 2013-05-14 18:38:14 +0000 |
|---|---|---|
| committer | herbelin | 2013-05-14 18:38:14 +0000 |
| commit | fd7448ad0f44ef306d910816d7b6d2f6a303f4a7 (patch) | |
| tree | 5a5c51c01bbbaa75a4ddffcca384cdf5cc7d0d2e /pretyping | |
| 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 'pretyping')
| -rw-r--r-- | pretyping/retyping.ml | 3 | ||||
| -rw-r--r-- | pretyping/typeclasses.ml | 2 | ||||
| -rw-r--r-- | pretyping/typing.ml | 4 |
3 files changed, 5 insertions, 4 deletions
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index bb1a366376..c618720912 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -168,7 +168,8 @@ let retype ?(polyprop=true) sigma = | _ -> family_of_sort (decomp_sort env sigma (type_of env t)) and type_of_global_reference_knowing_parameters env c args = - let argtyps = Array.map (fun c -> nf_evar sigma (type_of env c)) args in + let argtyps = + Array.map (fun c -> lazy (nf_evar sigma (type_of env c))) args in match kind_of_term c with | Ind ind -> let (_,mip) = lookup_mind_specif env ind in diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 9e2175624c..c14f107ec6 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -384,7 +384,7 @@ let add_inductive_class ind = let ctx = oneind.mind_arity_ctxt in let ty = Inductive.type_of_inductive_knowing_parameters (push_rel_context ctx (Global.env ())) - oneind (Termops.extended_rel_vect 0 ctx) + oneind (Array.map (fun x -> lazy x) (Termops.extended_rel_vect 0 ctx)) in { cl_impl = IndRef ind; cl_context = List.map (const None) ctx, ctx; diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 008b8b9a39..9fe95a1192 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 = |