Checker: factorize handling of typing flags

1 files changed, 1 insertions, 8 deletions

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 ->