diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/ftactic.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/tactics/ftactic.ml b/tactics/ftactic.ml index bbc739a3b4..43602d1fb6 100644 --- a/tactics/ftactic.ml +++ b/tactics/ftactic.ml @@ -38,8 +38,10 @@ let bind (type a) (type b) (m : a t) (f : a -> b t) : b t = m >>= function Proofview.tclUNIT (Depends (List.concat l)) let nf_enter f = - bind (Proofview.Goal.nf_goals >>= fun l -> Proofview.tclUNIT (Depends l)) - (fun gl -> Proofview.V82.wrap_exceptions (fun () -> f gl)) + bind (Proofview.Goal.goals >>= fun l -> Proofview.tclUNIT (Depends l)) + (fun gl -> + Proofview.Goal.normalize gl >>= fun nfgl -> + Proofview.V82.wrap_exceptions (fun () -> f nfgl)) let enter f = bind (Proofview.Goal.goals >>= fun l -> Proofview.tclUNIT (Depends l)) |