diff options
| -rw-r--r-- | kernel/safe_typing.ml | 2 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 2 | ||||
| -rw-r--r-- | library/global.ml | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 90b89995ee..779e05ee0c 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -1194,7 +1194,7 @@ loaded by side-effect once and for all (like it is done in OCaml). Would this be correct with respect to undo's and stuff ? *) -let set_strategy e k l = { e with env = +let set_strategy k l e = { e with env = (Environ.set_oracle e.env (Conv_oracle.set_strategy (Environ.oracle e.env) k l)) } diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index ea288b771e..443b5cfd73 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -218,4 +218,4 @@ val register : val register_inline : Constant.t -> safe_transformer0 val set_strategy : - safe_environment -> Names.Constant.t Names.tableKey -> Conv_oracle.level -> safe_environment + Names.Constant.t Names.tableKey -> Conv_oracle.level -> safe_transformer0 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) |