4 files changed, 6 insertions, 6 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index ee311ab24b..1c97806693 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 9a458f02ae..d9841085e1 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 cc7cf0c68a..a9cc151cf7 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 14ba95ec6e..d6484e8233 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 ->