diff options
Diffstat (limited to 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index b16d5b63d..dcdb866bf 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -155,3 +155,6 @@ val register : field -> Retroknowledge.entry -> Term.constr -> safe_transformer0 val register_inline : constant -> safe_transformer0 + +val set_strategy : + safe_environment -> 'a Names.tableKey -> Conv_oracle.level -> safe_environment |