diff options
| author | Gaëtan Gilbert | 2020-02-18 14:15:24 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-18 14:15:24 +0100 |
| commit | 5d535c7c624cc4ebae23b173254ba6492b33bee2 (patch) | |
| tree | 8c10b853a80a2e811c2a6f53f94766ad84242a16 /pretyping | |
| parent | af3fd09e2f0cc2eac2bc8802a6818baf0c184563 (diff) | |
Deprecate unsafe_type_of
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/typing.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/typing.mli b/pretyping/typing.mli index fd2dc7c2fc..e85f6327f8 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -19,6 +19,7 @@ open Evd (** Typecheck a term and return its type. May trigger an evarmap leak. *) val unsafe_type_of : env -> evar_map -> constr -> types +[@@ocaml.deprecated "Use [type_of] or retyping according to your needs."] (** Typecheck a term and return its type + updated evars, optionally refreshing universes *) |