From 22dfbff296cf03b6fab2bcec4eb5f9cf6ee8368c Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 4 Nov 2016 15:55:52 +0100
Subject: Fix #3441 Use pf_get_type_of to avoid blowup

... in pose proof of large proof terms
---
 tactics/tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

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 }
-- 
cgit v1.2.3