Merge PR #11623: Deprecate unsafe_type_of

Reviewed-by: maximedenes
Reviewed-by: ppedrot

3 files changed, 11 insertions, 4 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 *)
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index d3bce07814..3e4549f92c 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -76,7 +76,6 @@ let pf_nf                        = pf_reduce simpl
 let pf_nf_betaiota               = pf_reduce nf_betaiota
 let pf_compute                   = pf_reduce compute
 let pf_unfoldn ubinds            = pf_reduce (unfoldn ubinds)
-let pf_unsafe_type_of            = pf_reduce unsafe_type_of
 let pf_type_of                   = pf_reduce type_of
 let pf_get_type_of               = pf_reduce Retyping.get_type_of
 
@@ -117,9 +116,6 @@ module New = struct
   let pf_env = Proofview.Goal.env
   let pf_concl = Proofview.Goal.concl
 
-  let pf_unsafe_type_of gl t =
-    pf_apply unsafe_type_of gl t
-
   let pf_type_of gl t =
     pf_apply type_of gl t
 
@@ -182,4 +178,12 @@ module New = struct
   let pf_compute gl t = pf_apply compute gl t
 
   let pf_nf_evar gl t = nf_evar (project gl) t
+
+  (* deprecated *)
+  let pf_unsafe_type_of gl t =
+    pf_apply (unsafe_type_of[@warning "-3"]) gl t
+
 end
+
+(* deprecated *)
+let pf_unsafe_type_of            = pf_reduce unsafe_type_of[@warning "-3"]
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index aed1c89bfe..b4247f39b9 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -34,6 +34,7 @@ val pf_nth_hyp_id         : Goal.goal sigma -> int -> Id.t
 val pf_last_hyp           : Goal.goal sigma -> named_declaration
 val pf_ids_of_hyps        : Goal.goal sigma -> Id.t list
 val pf_unsafe_type_of     : Goal.goal sigma -> constr -> types
+[@@ocaml.deprecated "Use [type_of] or retyping according to your needs."]
 val pf_type_of            : Goal.goal sigma -> constr -> evar_map * types
 val pf_hnf_type_of        : Goal.goal sigma -> constr -> types
 
@@ -83,6 +84,7 @@ module New : sig
   (** WRONG: To be avoided at all costs, it typechecks the term entirely but
      forgets the universe constraints necessary to retypecheck it *)
   val pf_unsafe_type_of : Proofview.Goal.t -> constr -> types
+  [@@ocaml.deprecated "Use [type_of] or retyping according to your needs."]
 
   (** This function does no type inference and expects an already well-typed term.
       It recomputes its type in the fastest way possible (no conversion is ever involved) *)