diff options
| -rw-r--r-- | pretyping/typing.mli | 1 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 12 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 2 |
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) *) |