diff options
| author | herbelin | 2013-05-14 18:38:14 +0000 |
|---|---|---|
| committer | herbelin | 2013-05-14 18:38:14 +0000 |
| commit | fd7448ad0f44ef306d910816d7b6d2f6a303f4a7 (patch) | |
| tree | 5a5c51c01bbbaa75a4ddffcca384cdf5cc7d0d2e /kernel/inductive.ml | |
| parent | 23a51bab686dd0ceaa9a87b09beb49d0ee0575c4 (diff) | |
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
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 2 |
1 files changed, 1 insertions, 1 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, [] -> |