diff options
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 87c139f48..a02d5e205 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -165,7 +165,10 @@ let rec make_subst env = (* 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 (Lazy.force a))) in - make (cons_subst u s subst) (sign, exp, args) + if Univ.Universe.is_levels s then + make (cons_subst u s subst) (sign, exp, args) + else (* Cannot handle substitution by i+n universes. *) + make subst (sign, exp, args) | (na,None,t)::sign, Some u::exp, [] -> (* No more argument here: we add the remaining universes to the *) (* substitution (when [u] is distinct from all other universes in the *) |