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 764dfcc7b..e9f8f89ad 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -262,7 +262,7 @@ let typecheck_inductive env mie = Inl (info,full_arity,s), enforce_geq u lev cst | Prop Pos when engagement env <> Some ImpredicativeSet -> (* Predicative set: check that the content is indeed predicative *) - if not (is_lower_univ lev) & not (is_type0_univ lev) then + if not (is_type0m_univ lev) & not (is_type0_univ lev) then error "Large non-propositional inductive types must be in Type"; Inl (info,full_arity,s), cst | Prop _ -> |