From 2ac3d11f6f1332250e918ef628eca3b788b3550a Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 16 Oct 2020 20:06:26 +0200
Subject: [environ] [typing_flags] Introduce helper function to remove
 duplicate code

---
 kernel/environ.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'kernel/environ.mli')

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 }
-- 
cgit v1.2.3