diff options
| author | Pierre-Marie Pédrot | 2020-02-24 18:11:58 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-02-24 18:11:58 +0100 |
| commit | 00a3dcc11342e1304f078e1457dcfd118dc4e573 (patch) | |
| tree | 8bfedced5772616dbe97f80a3ae29cff9180f3b5 /pretyping | |
| parent | 5fd281945bdc60c2a88f60503663df32920ef83b (diff) | |
| parent | 5d535c7c624cc4ebae23b173254ba6492b33bee2 (diff) | |
Merge PR #11623: Deprecate unsafe_type_of
Reviewed-by: maximedenes
Reviewed-by: ppedrot
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 *) |