diff options
Diffstat (limited to 'kernel/declarations.ml')
| -rw-r--r-- | kernel/declarations.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 282dad0da..fc8064d59 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -210,7 +210,7 @@ type mutual_inductive_body = { } let subst_arity sub arity = - if sub = empty_subst then arity + if is_empty_subst sub then arity else match arity with | NonPolymorphicType s -> NonPolymorphicType (subst_mps sub s) | PolymorphicArity (ctx,s) -> PolymorphicArity (subst_rel_context sub ctx,s) |