Fix #3441 Use pf_get_type_of to avoid blowup

... in pose proof of large proof terms

1 files changed, 1 insertions, 1 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 548d2a81f3..92cb8a11ea 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2714,7 +2714,7 @@ let forward b usetac ipat c =
   match usetac with
   | None ->
       Proofview.Goal.enter { enter = begin fun gl ->
-      let t = Tacmach.New.pf_unsafe_type_of gl c in
+      let t = Tacmach.New.pf_get_type_of gl c in
       let hd = head_ident c in
       Tacticals.New.tclTHENFIRST (assert_as true hd ipat t) (exact_no_check c)
       end }