diff options
Diffstat (limited to 'kernel/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 31c0e83c8..9c79009db 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -173,7 +173,7 @@ let cumulate_arity_large_levels env sign = sign (Universe.type0m,env)) let is_impredicative env u = - is_type0m_univ u || (is_type0_univ u && engagement env = Some ImpredicativeSet) + is_type0m_univ u || (is_type0_univ u && is_impredicative_set env) (* Returns the list [x_1, ..., x_n] of levels contributing to template polymorphism. The elements x_k is None if the k-th parameter (starting |