unsafe_type_of -> type_of in Celenv.mk_clenv_type_of

1 files changed, 5 insertions, 1 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index e466992721..bb660adf4d 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -128,7 +128,11 @@ let mk_clenv_from_n gls n (c,cty) =
 
 let mk_clenv_from gls = mk_clenv_from_n gls None
 
-let mk_clenv_type_of gls t = mk_clenv_from gls (t,Tacmach.New.pf_unsafe_type_of gls t)
+let mk_clenv_type_of gls t =
+  let env = Proofview.Goal.env gls in
+  let sigma = Tacmach.New.project gls in
+  let sigma, tt = Typing.type_of env sigma t in
+  mk_clenv_from_env env sigma None (t,tt)
 
 (******************************************************************)