unsafe_type_of -> type_of in Tactics.convert_concl

1 files changed, 3 insertions, 2 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f6f7c71dfd..a44d83141e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -151,11 +151,12 @@ let convert_concl ~check ty k =
     Refine.refine ~typecheck:false begin fun sigma ->
       let sigma =
         if check then begin
-          ignore (Typing.unsafe_type_of env sigma ty);
+          let sigma, _ = Typing.type_of env sigma ty in
           match Reductionops.infer_conv env sigma ty conclty with
           | None -> error "Not convertible."
           | Some sigma -> sigma
-        end else sigma in
+        end else sigma
+      in
       let (sigma, x) = Evarutil.new_evar env sigma ~principal:true ty in
       let ans = if k == DEFAULTcast then x else mkCast(x,k,conclty) in
       (sigma, ans)