unsafe_type_of -> get_type_of in Equality.inject_if_homogenous_dependent_pair

1 files changed, 1 insertions, 1 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index de7e755e5a..9195746dc6 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1352,7 +1352,7 @@ let inject_if_homogenous_dependent_pair ty =
     if not (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) ind &&
       pf_apply is_conv gl ar1.(2) ar2.(2)) then raise Exit;
     check_required_library ["Coq";"Logic";"Eqdep_dec"];
-    let new_eq_args = [|pf_unsafe_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in
+    let new_eq_args = [|pf_get_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in
     let inj2 = lib_ref "core.eqdep_dec.inj_pair2" in
     let c, eff = find_scheme (!eq_dec_scheme_kind_name()) ind in
     (* cut with the good equality and prove the requested goal *)