diff options
Diffstat (limited to 'checker/mod_checking.ml')
| -rw-r--r-- | checker/mod_checking.ml | 10 |
1 files changed, 1 insertions, 9 deletions
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 44b7089fd0..2f795ff8d9 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 -> @@ -84,7 +77,6 @@ let mk_mtb mp sign delta = mod_expr = (); mod_type = sign; mod_type_alg = None; - mod_constraints = Univ.ContextSet.empty; mod_delta = delta; mod_retroknowledge = ModTypeRK; } |