From 83ebacdb7f307451fc801637224c911eb0da9fea Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Mon, 15 Sep 2014 16:46:08 +0200
Subject: 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).
---
 tactics/ftactic.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'tactics')

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))
-- 
cgit v1.2.3