From fd7448ad0f44ef306d910816d7b6d2f6a303f4a7 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 14 May 2013 18:38:14 +0000
Subject: 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
---
 kernel/inductive.ml  | 2 +-
 kernel/inductive.mli | 4 ++--
 kernel/typeops.ml    | 4 ++--
 kernel/typeops.mli   | 2 +-
 4 files changed, 6 insertions(+), 6 deletions(-)

(limited to 'kernel')

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 ->
-- 
cgit v1.2.3