diff options
Diffstat (limited to 'checker/mod_checking.ml')
| -rw-r--r-- | checker/mod_checking.ml | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 9b41fbcb7a..09b8c48c15 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -17,9 +17,12 @@ 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); - (* Locally set the oracle for further typechecking *) - let oracle = env.env_typing_flags.conv_oracle in - let env = Environ.set_oracle env cb.const_typing_flags.conv_oracle in + (* Locally set typing flags for further typechecking *) + let orig_flags = env.env_typing_flags in + let cb_flags = cb.const_typing_flags in + let env = Environ.set_typing_flags {orig_flags with check_guarded = cb_flags.check_guarded; + check_universes = cb_flags.check_universes; + conv_oracle = cb_flags.conv_oracle} env in (* [env'] contains De Bruijn universe variables *) let poly, env' = match cb.const_universes with @@ -57,8 +60,8 @@ let check_constant_declaration env kn cb = if poly then add_constant kn cb env else add_constant kn cb env' in - (* Reset the value of the oracle *) - Environ.set_oracle env oracle + (* Reset the value of the typing flags *) + Environ.set_typing_flags orig_flags env (** {6 Checking modules } *) |