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 9a11e47dc..9d2580ce4 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -282,7 +282,7 @@ let typecheck_inductive env mie = | _ -> true end -> (* Predicative set: check that the content is indeed predicative *) - if not (is_type0m_univ lev) & not (is_type0_univ lev) then + if not (is_type0m_univ lev) && not (is_type0_univ lev) then raise (InductiveError LargeNonPropInductiveNotInType); Inl (info,full_arity,s), cst | Prop _ -> |