[kernel] Allow to set typing flags in add_constant

This is just an experiment, but makes the uses of the API easier as we
don't mess with the global state anymore.

1 files changed, 12 insertions, 0 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 6abd283f6c..1ecb5cba7d 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -247,6 +247,15 @@ let set_native_compiler b senv =
 
 let set_allow_sprop b senv = { senv with env = Environ.set_allow_sprop b senv.env }
 
+(* Temporary sets custom typing flags *)
+let with_typing_flags ?typing_flags senv ~f =
+  match typing_flags with
+  | None -> f senv
+  | Some typing_flags ->
+    let orig_typing_flags = Environ.typing_flags senv.env in
+    let res, senv = f (set_typing_flags typing_flags senv) in
+    res, set_typing_flags orig_typing_flags senv
+
 (** Check that the engagement [c] expected by a library matches
     the current (initial) one *)
 let check_engagement env expected_impredicative_set =
@@ -928,6 +937,9 @@ let add_constant l decl senv =
   in
   kn, senv
 
+let add_constant ?typing_flags l decl senv =
+  with_typing_flags ?typing_flags senv ~f:(add_constant l decl)
+
 let add_private_constant l decl senv : (Constant.t * private_constants) * safe_environment =
   let kn = Constant.make2 senv.modpath l in
     let cb =