Fix timing of evar-normalisation of goals in [Ftactic.nf_enter].

All goals were normalised up front, rather than normalised after the tactic acting on previous goal had the chance to solve some evars, which then appeared non-instantiated to tactics which do not work up to evar map (most of them).

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))