From 5d535c7c624cc4ebae23b173254ba6492b33bee2 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 18 Feb 2020 14:15:24 +0100
Subject: Deprecate unsafe_type_of

---
 pretyping/typing.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'pretyping')

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 *)
-- 
cgit v1.2.3