diff options
Diffstat (limited to 'tactics')
| -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 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 } |
