aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/tactics.ml2
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 }