From 9655b3413544319e1bb6633744c67d6ddc303f1d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 6 Feb 2020 14:39:59 +0100
Subject: unsafe_type_of -> type_of in Tactics.convert_concl

---
 tactics/tactics.ml | 5 +++--
 1 file 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)
-- 
cgit v1.2.3