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 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/inductive.ml')

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