diff options
| -rw-r--r-- | kernel/inductive.ml | 2 | ||||
| -rw-r--r-- | kernel/inductive.mli | 4 | ||||
| -rw-r--r-- | kernel/typeops.ml | 4 | ||||
| -rw-r--r-- | kernel/typeops.mli | 2 | ||||
| -rw-r--r-- | pretyping/retyping.ml | 3 | ||||
| -rw-r--r-- | pretyping/typeclasses.ml | 2 | ||||
| -rw-r--r-- | pretyping/typing.ml | 4 |
7 files changed, 11 insertions, 10 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index ee311ab24..1c9780669 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -148,7 +148,7 @@ let rec make_subst env = function (* arity is a global level which, at typing time, will be enforce *) (* to be greater than the level of the argument; this is probably *) (* a useless extra constraint *) - let s = sort_as_univ (snd (dest_arity env a)) in + let s = sort_as_univ (snd (dest_arity env (Lazy.force a))) in let ctx,subst = make_subst env (sign, exp, args) in d::ctx, cons_subst u s subst | (na,None,t as d)::sign, Some u::exp, [] -> diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 9a458f02a..d9841085e 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -93,12 +93,12 @@ val check_cofix : env -> cofixpoint -> unit exception SingletonInductiveBecomesProp of Id.t val type_of_inductive_knowing_parameters : ?polyprop:bool -> - env -> one_inductive_body -> types array -> types + env -> one_inductive_body -> types Lazy.t array -> types val max_inductive_sort : sorts array -> universe val instantiate_universes : env -> rel_context -> - polymorphic_arity -> types array -> rel_context * sorts + polymorphic_arity -> types Lazy.t array -> rel_context * sorts (** {6 Debug} *) 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 diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 14ba95ec6..d6484e823 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -101,7 +101,7 @@ val type_of_constant : env -> constant -> types val type_of_constant_type : env -> constant_type -> types val type_of_constant_knowing_parameters : - env -> constant_type -> constr array -> types + env -> constant_type -> types Lazy.t array -> types (** Make a type polymorphic if an arity *) val make_polymorphic_if_constant_for_ind : env -> unsafe_judgment -> diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index bb1a36637..c61872091 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 9e2175624..c14f107ec 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 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 = |