diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
commit | 9ebf44d84754adc5b64fcf612c6816c02c80462d (patch) | |
tree | bf5e06a28488e0e06a2f2011ff0d110e2e02f8fc /library/global.ml | |
parent | 9043add656177eeac1491a73d2f3ab92bec0013c (diff) |
Imported Upstream version 8.9.0upstream/8.9.0upstream
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 dcb20a28..e833f711 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 |