[kernel] Allow to set typing flags in add_mind [inductive]

2 files changed, 4 insertions, 0 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 1ecb5cba7d..a35f94e3ce 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -995,6 +995,9 @@ let add_mind l mie senv =
   let mib = Indtypes.check_inductive senv.env ~sec_univs kn mie in
   kn, add_checked_mind kn mib senv
 
+let add_mind ?typing_flags l mie senv =
+  with_typing_flags ?typing_flags senv ~f:(add_mind l mie)
+
 (** Insertion of module types *)
 
 let add_modtype l params_mte inl senv =
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index c4d0fffe2b..287274e39a 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -103,6 +103,7 @@ val add_private_constant :
 (** Adding an inductive type *)
 
 val add_mind :
+  ?typing_flags:Declarations.typing_flags ->
   Label.t -> Entries.mutual_inductive_entry ->
     MutInd.t safe_transformer