From 34d95672ecace6733d9d2f738ee6d7aee46fb2d0 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 6 Feb 2020 16:06:03 +0100
Subject: unsafe_type_of -> get_type_of in Hints.make_trivial

---
 tactics/hints.ml | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

(limited to 'tactics/hints.ml')

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