aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/safe_typing.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/safe_typing.ml')
-rw-r--r--kernel/safe_typing.ml4
1 files changed, 4 insertions, 0 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 40f16a6e6..3132d45e3 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -777,3 +777,7 @@ environment, and store for the future (instead of just its type)
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 =
+ (Environ.set_oracle e.env
+ (Conv_oracle.set_strategy (Environ.oracle e.env) k l)) }