diff options
| author | Maxime Dénès | 2018-10-31 16:12:26 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-10-31 16:16:41 +0100 |
| commit | c367e7cd962089d2932b986e5764b8e3844ad4b0 (patch) | |
| tree | 55f75f93217a8f41c972b6f9514b62bdad1f1b30 /library/global.ml | |
| parent | c3ea3cd8a2bd29fc0129e34af4a1689bbf7519a5 (diff) | |
Use standard combinator for Global.set_strategy
Diffstat (limited to 'library/global.ml')
| -rw-r--r-- | library/global.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/global.ml b/library/global.ml index 6461b4c37f..bfea6d3dea 100644 --- a/library/global.ml +++ b/library/global.ml @@ -182,7 +182,7 @@ let register field value = 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) + globalize0 (Safe_typing.set_strategy k l) let set_share_reduction b = globalize0 (Safe_typing.set_share_reduction b) |