diff options
author | 2016-11-04 15:55:52 +0100 | |
---|---|---|
committer | 2016-11-04 16:00:52 +0100 | |
commit | 22dfbff296cf03b6fab2bcec4eb5f9cf6ee8368c (patch) | |
tree | 096a4ff4fec84349501f2f94f4011432337a8a5e /tactics/tactics.ml | |
parent | 6bb352a6743c7332b9715ac15e95c806a58d101c (diff) |
Fix #3441 Use pf_get_type_of to avoid blowup
... in pose proof of large proof terms
Diffstat (limited to 'tactics/tactics.ml')
-rw-r--r-- | tactics/tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 548d2a81f..92cb8a11e 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 } |