unsafe_type_of -> get_type_of in Hints.make_trivial

1 files changed, 9 insertions, 9 deletions

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 7b3797119a..73e8331bcb 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -26,7 +26,6 @@ open Libnames
 open Smartlocate
 open Termops
 open Inductiveops
-open Typing
 open Typeclasses
 open Pattern
 open Patternops
@@ -966,16 +965,17 @@ let make_mode ref m =
 let make_trivial env sigma poly ?(name=PathAny) r =
   let c,ctx = fresh_global_or_constr env sigma poly r in
   let sigma = Evd.merge_context_set univ_flexible sigma ctx in
-  let t = hnf_constr env sigma (unsafe_type_of env sigma c) in
+  let t = hnf_constr env sigma (Retyping.get_type_of env sigma c) in
   let hd = head_constr sigma t in
   let ce = mk_clenv_from_env env sigma None (c,t) in
-  (Some hd, { pri=1;
-              poly = poly;
-              pat = Some (Patternops.pattern_of_constr env ce.evd (EConstr.to_constr sigma (clenv_type ce)));
-              name = name;
-              db = None;
-              secvars = secvars_of_constr env sigma c;
-              code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx)) })
+  (Some hd,
+   { pri=1;
+     poly = poly;
+     pat = Some (Patternops.pattern_of_constr env ce.evd (EConstr.to_constr sigma (clenv_type ce)));
+     name = name;
+     db = None;
+     secvars = secvars_of_constr env sigma c;
+     code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx)) })