From 5a9e90e426ba2e25cbcb76af2bb67717984e2b6b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 15 Oct 2020 16:48:38 +0200
Subject: [kernel] Allow to set typing flags in add_mind [inductive]

---
 kernel/safe_typing.ml  | 3 +++
 kernel/safe_typing.mli | 1 +
 library/global.ml      | 2 +-
 library/global.mli     | 1 +
 4 files changed, 6 insertions(+), 1 deletion(-)

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
 
diff --git a/library/global.ml b/library/global.ml
index 238b9d554b..71cadb3600 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -107,7 +107,7 @@ let sprop_allowed () = Environ.sprop_allowed (env())
 let export_private_constants cd = globalize (Safe_typing.export_private_constants cd)
 let add_constant ?typing_flags id d = globalize (Safe_typing.add_constant ?typing_flags (i2l id) d)
 let add_private_constant id d = globalize (Safe_typing.add_private_constant (i2l id) d)
-let add_mind id mie = globalize (Safe_typing.add_mind (i2l id) mie)
+let add_mind ?typing_flags id mie = globalize (Safe_typing.add_mind ?typing_flags (i2l id) mie)
 let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl)
 let add_module id me inl = globalize (Safe_typing.add_module (i2l id) me inl)
 let add_include me ismod inl = globalize (Safe_typing.add_include me ismod inl)
diff --git a/library/global.mli b/library/global.mli
index 4c2d427925..c9b9d7f536 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -57,6 +57,7 @@ val add_constant :
 val add_private_constant :
   Id.t -> Safe_typing.side_effect_declaration -> Constant.t * Safe_typing.private_constants
 val add_mind :
+  ?typing_flags:Declarations.typing_flags ->
   Id.t -> Entries.mutual_inductive_entry -> MutInd.t
 
 (** Extra universe constraints *)
-- 
cgit v1.2.3