From 988e195c2cd0d97b664193bf1c83c3da2b380f7c Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 6 Apr 2020 14:40:11 +0200
Subject: Checker: factorize handling of typing flags

---
 checker/mod_checking.ml | 9 +--------
 1 file changed, 1 insertion(+), 8 deletions(-)

(limited to 'checker/mod_checking.ml')

diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 44b7089fd0..8fd81d43be 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -17,14 +17,7 @@ let set_indirect_accessor f = indirect_accessor := f
 
 let check_constant_declaration env kn cb =
   Flags.if_verbose Feedback.msg_notice (str "  checking cst:" ++ Constant.print kn);
-  let cb_flags = cb.const_typing_flags in
-  let env = Environ.set_typing_flags
-      {env.env_typing_flags with
-       check_guarded = cb_flags.check_guarded;
-       check_universes = cb_flags.check_universes;
-       conv_oracle = cb_flags.conv_oracle;}
-      env
-  in
+  let env = CheckFlags.set_local_flags cb.const_typing_flags env in
   let poly, env =
     match cb.const_universes with
     | Monomorphic ctx ->
-- 
cgit v1.2.3