From c367e7cd962089d2932b986e5764b8e3844ad4b0 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 31 Oct 2018 16:12:26 +0100 Subject: Use standard combinator for Global.set_strategy --- library/global.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'library') 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) -- cgit v1.2.3