From 42c28946cded7e81ade816416fc1538341fd4da8 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 6 Feb 2020 16:37:33 +0100
Subject: unsafe_type_of -> get_type_of in Elim.general_decomposer + pf_apply
 in ifOnHyp

---
 tactics/elim.ml       | 7 ++-----
 tactics/tacticals.ml  | 2 +-
 tactics/tacticals.mli | 2 +-
 3 files changed, 4 insertions(+), 7 deletions(-)

diff --git a/tactics/elim.ml b/tactics/elim.ml
index ea61b8e4df..c0d533a6f2 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -80,14 +80,11 @@ let up_to_delta = ref false (* true *)
 
 let general_decompose recognizer c =
   Proofview.Goal.enter begin fun gl ->
-  let type_of = pf_unsafe_type_of gl in
-  let env = pf_env gl in
-  let sigma = project gl in
-  let typc = type_of c in
+  let typc = pf_get_type_of gl c in
   tclTHENS (cut typc)
     [ tclTHEN (intro_using tmphyp_name)
          (onLastHypId
-            (ifOnHyp (recognizer env sigma) (general_decompose_aux (recognizer env sigma))
+            (ifOnHyp recognizer (general_decompose_aux recognizer)
               (fun id -> clear [id])));
        exact_no_check c ]
   end
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 199fdd50c4..58d2097dea 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -587,7 +587,7 @@ module New = struct
   let ifOnHyp pred tac1 tac2 id =
     Proofview.Goal.enter begin fun gl ->
     let typ = Tacmach.New.pf_get_hyp_typ id gl in
-    if pred (id,typ) then
+    if pf_apply pred gl (id,typ) then
       tac1 id
     else
       tac2 id
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 31d26834d6..4b93b81d1c 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -222,7 +222,7 @@ module New : sig
 
   val nLastDecls  : Proofview.Goal.t -> int -> named_context
 
-  val ifOnHyp     : (Id.t * types -> bool) ->
+  val ifOnHyp : (Environ.env -> evar_map -> Id.t * types -> bool) ->
     (Id.t -> unit Proofview.tactic) -> (Id.t -> unit Proofview.tactic) ->
     Id.t -> unit Proofview.tactic
 
-- 
cgit v1.2.3