[environ] [typing_flags] Introduce helper function to remove duplicate code

2 files changed, 6 insertions, 0 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 69edb1498c..a5f81d1e59 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -479,6 +479,9 @@ let set_typing_flags c env =
     let env = set_type_in_type (not c.check_universes) env in
     env
 
+let update_typing_flags ?typing_flags env =
+  Option.cata (fun flags -> set_typing_flags flags env) env typing_flags
+
 let set_cumulative_sprop b env =
   set_typing_flags {env.env_typing_flags with cumulative_sprop=b} env
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 6a8ddce835..900e2128ea 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -351,6 +351,9 @@ val set_type_in_type : bool -> env -> env
 val set_allow_sprop : bool -> env -> env
 val sprop_allowed : env -> bool
 
+(** [update_typing_flags ?typing_flags] may update env with optional typing flags *)
+val update_typing_flags : ?typing_flags:typing_flags -> env -> env
+
 val universes_of_global : env -> GlobRef.t -> AUContext.t
 
 (** {6 Sets of referred section variables }