From 3fcf06878d10a4a0c17d7095da964ebf15ed922b Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 6 Feb 2020 14:40:57 +0100
Subject: unsafe_type_of -> type_of in Tactics.change_on_subterm

---
 tactics/tactics.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index a44d83141e..b0ee02a631 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -850,12 +850,13 @@ let change_on_subterm ~check cv_pb deep t where env sigma c =
             change_and_check Reduction.CONV mayneedglobalcheck true (t subst)
           else
             fun env sigma _c -> t subst env sigma) env sigma c in
-  if !mayneedglobalcheck then
+  let sigma = if !mayneedglobalcheck then
     begin
-      try ignore (Typing.unsafe_type_of env sigma c)
+      try fst (Typing.type_of env sigma c)
       with e when catchable_exception e ->
         error "Replacement would lead to an ill-typed term."
-    end;
+    end else sigma
+  in
   (sigma, c)
 
 let change_in_concl ~check occl t =
-- 
cgit v1.2.3