diff options
Diffstat (limited to 'tactics/ftactic.ml')
| -rw-r--r-- | tactics/ftactic.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/ftactic.ml b/tactics/ftactic.ml index 43602d1fb..d8b12fc4e 100644 --- a/tactics/ftactic.ml +++ b/tactics/ftactic.ml @@ -40,12 +40,13 @@ let bind (type a) (type b) (m : a t) (f : a -> b t) : b t = m >>= function let nf_enter f = bind (Proofview.Goal.goals >>= fun l -> Proofview.tclUNIT (Depends l)) (fun gl -> + gl >>= 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)) - (fun gl -> Proofview.V82.wrap_exceptions (fun () -> f gl)) + (fun gl -> gl >>= fun gl -> Proofview.V82.wrap_exceptions (fun () -> f gl)) let lift (type a) (t:a Proofview.tactic) : a t = Proofview.tclBIND t (fun x -> Proofview.tclUNIT (Uniform x)) |