diff options
Diffstat (limited to 'library')
| -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) |