Use thunks to univ instead of lazy constr for template typing

6 files changed, 30 insertions, 13 deletions

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 816a8c4703..a4406aeba1 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -29,7 +29,7 @@ open Context.Rel.Declaration
 let type_of_inductive env (ind,u) =
  let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
  Typeops.check_hyps_inclusion env (GlobRef.IndRef ind) mib.mind_hyps;
- Inductive.type_of_inductive env (specif,u)
+ Inductive.type_of_inductive (specif,u)
 
 (* Return type as quoted by the user *)
 let type_of_constructor env (cstr,u) =
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index bfee07e7f0..838bf22c66 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1707,7 +1707,7 @@ let splay_arity env sigma c =
   let l, c = splay_prod env sigma c in
   match EConstr.kind sigma c with
     | Sort s -> l,s
-    | _ -> invalid_arg "splay_arity"
+    | _ -> raise Reduction.NotArity
 
 let sort_of_arity env sigma c = snd (splay_arity env sigma c)
 
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index e72f5f2793..c539ec55ed 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -236,12 +236,20 @@ val hnf_lam_applist  : env ->  evar_map -> constr -> constr list -> constr
 
 val splay_prod : env ->  evar_map -> constr -> (Name.t Context.binder_annot * constr) list * constr
 val splay_lam : env ->  evar_map -> constr -> (Name.t Context.binder_annot * constr) list * constr
+val splay_prod_assum : env ->  evar_map -> constr -> rel_context * constr
+
 val splay_arity : env ->  evar_map -> constr -> (Name.t Context.binder_annot * constr) list * ESorts.t
+(** Raises [Reduction.NotArity] *)
+
 val sort_of_arity : env -> evar_map -> constr -> ESorts.t
+(** Raises [Reduction.NotArity] *)
+
 val splay_prod_n : env ->  evar_map -> int -> constr -> rel_context * constr
+(** Raises [Invalid_argument] *)
+
 val splay_lam_n : env ->  evar_map -> int -> constr -> rel_context * constr
-val splay_prod_assum :
-  env ->  evar_map -> constr -> rel_context * constr
+(** Raises [Invalid_argument] *)
+
 
 type 'a miota_args = {
   mP      : constr;     (** the result type *)
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index d2af957b54..87fe4cfcda 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -168,15 +168,21 @@ let retype ?(polyprop=true) sigma =
     | _ -> decomp_sort env sigma (type_of env t)
 
   and type_of_global_reference_knowing_parameters env c args =
-    let argtyps =
-      Array.map (fun c -> lazy (EConstr.to_constr ~abort_on_undefined_evars:false sigma (type_of env c))) args in
     match EConstr.kind sigma c with
     | Ind (ind, u) ->
       let u = EInstance.kind sigma u in
       let mip = lookup_mind_specif env ind in
-        EConstr.of_constr (try Inductive.type_of_inductive_knowing_parameters
-               ~polyprop env (mip, u) argtyps
-         with Reduction.NotArity -> retype_error NotAnArity)
+      let paramtyps = Array.map_to_list (fun arg () ->
+          let t = type_of env arg in
+          let s = try Reductionops.sort_of_arity env sigma t
+            with Reduction.NotArity -> retype_error NotAnArity
+          in
+          Sorts.univ_of_sort (ESorts.kind sigma s))
+          args
+      in
+      EConstr.of_constr
+        (Inductive.type_of_inductive_knowing_parameters
+           ~polyprop (mip, u) paramtyps)
     | Construct (cstr, u) ->
       let u = EInstance.kind sigma u in
       EConstr.of_constr (type_of_constructor env (cstr, u))
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index b4c19775a7..f067c075bf 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -38,8 +38,11 @@ let meta_type evd mv =
 let inductive_type_knowing_parameters env sigma (ind,u) jl =
   let u = Unsafe.to_instance u in
   let mspec = lookup_mind_specif env ind in
-  let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr ~abort_on_undefined_evars:false sigma j.uj_type)) jl in
-  Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp
+  let paramstyp = Array.map_to_list (fun j () ->
+      let s = Reductionops.sort_of_arity env sigma j.uj_type in
+      Sorts.univ_of_sort (EConstr.ESorts.kind sigma s)) jl
+  in
+  Inductive.type_of_inductive_knowing_parameters (mspec,u) paramstyp
 
 let type_judgment env sigma j =
   match EConstr.kind sigma (whd_all env sigma j.uj_type) with
@@ -307,7 +310,7 @@ let type_of_inductive env sigma (ind,u) =
   let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
   let () = check_hyps_inclusion env sigma (GR.IndRef ind) mib.mind_hyps in
   let u = EInstance.kind sigma u in
-  let ty, csts = Inductive.constrained_type_of_inductive env (specif,u) in
+  let ty, csts = Inductive.constrained_type_of_inductive (specif,u) in
   let sigma = Evd.add_constraints sigma csts in
   sigma, (EConstr.of_constr (rename_type ty (GR.IndRef ind)))
 
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 885fc8980d..b04e59734d 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -98,7 +98,7 @@ let construct_of_constr_const env tag typ =
 let construct_of_constr_block = construct_of_constr false
 
 let type_of_ind env (ind, u) =
-  type_of_inductive env (Inductive.lookup_mind_specif env ind, u)
+  type_of_inductive (Inductive.lookup_mind_specif env ind, u)
 
 let build_branches_type env sigma (mind,_ as _ind) mib mip u params p =
   let rtbl = mip.mind_reloc_tbl in