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 =