diff options
Diffstat (limited to 'kernel/declarations.mli')
| -rw-r--r-- | kernel/declarations.mli | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.mli index ef4d398c1f..f89773fcc5 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -190,11 +190,8 @@ type mutual_inductive_body = { mind_universes : Univ.universe_context; (** Local universe variables and constraints *) mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *) - - mind_checked_positive : bool; (** [false] when the mutual-inductive was assumed to be well-founded, bypassing the positivity checker. *) - - mind_unsafe_universes : bool; (** generated with the type-in-type flag *) + mind_typing_flags : typing_flags; (** typing flags at the time of the inductive creation *) } (** {6 Module declarations } *) |