diff options
| author | Pierre-Marie Pédrot | 2018-03-27 16:16:40 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-07-26 13:50:10 +0200 |
| commit | de20a45db5d45154819f2ed4359effdbb8bf0292 (patch) | |
| tree | 4df0add753c3464868f3bc61350cdd9ff7dc445a /library/global.ml | |
| parent | 09c76adaff7adaada1c49479dfa9a4d0a4b416af (diff) | |
Turn the kernel reduction sharing flag into an argument passed in the cache.
We move the global declaration of that argument to the environment, and reuse
the Global module to handle this flag.
Note that the checker was not using this flag before this patch, and still
doesn't use it. This should probably be fixed in a later patch.
Diffstat (limited to 'library/global.ml')
| -rw-r--r-- | library/global.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/library/global.ml b/library/global.ml index dcb20a280e..e833f71142 100644 --- a/library/global.ml +++ b/library/global.ml @@ -90,6 +90,7 @@ let push_context b c = globalize0 (Safe_typing.push_context b c) let set_engagement c = globalize0 (Safe_typing.set_engagement c) let set_typing_flags c = globalize0 (Safe_typing.set_typing_flags c) +let typing_flags () = Environ.typing_flags (env ()) let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd) let add_constant dir id d = globalize (Safe_typing.add_constant dir (i2l id) d) let add_mind dir id mie = globalize (Safe_typing.add_mind dir (i2l id) mie) @@ -278,3 +279,9 @@ let register_inline c = globalize0 (Safe_typing.register_inline c) let set_strategy k l = GlobalSafeEnv.set_safe_env (Safe_typing.set_strategy (safe_env ()) k l) +let set_reduction_sharing b = + let env = safe_env () in + let flags = Environ.typing_flags (Safe_typing.env_of_safe_env env) in + let flags = { flags with Declarations.share_reduction = b } in + let env = Safe_typing.set_typing_flags flags env in + GlobalSafeEnv.set_safe_env env |