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

3 files changed, 13 insertions, 19 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index a97add1ce7..75725e47c4 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -911,6 +911,12 @@ module Goal = struct
         tclZERO e
     end
 
+  let normalize { self } =
+    Proof.current >>= fun env ->
+    tclEVARMAP >>= fun sigma ->
+    let (gl,sigma) = Goal.eval nf_enter_t env sigma self in
+    tclTHEN (V82.tclEVARS sigma) (tclUNIT gl)
+
   let enter_t f = Goal.enter begin fun env sigma concl self ->
     f {env=env;sigma=sigma;concl=concl;self=self}
   end
@@ -928,20 +934,6 @@ module Goal = struct
         tclZERO e
     end
 
-  let nf_goals =
-    Proof.current >>= fun env ->
-    Proof.get >>= fun step ->
-    let sigma = step.solution in
-    let map goal =
-      match Goal.advance sigma goal with
-      | None -> None (** ppedrot: Is this check really necessary? *)
-      | Some goal ->
-        (** The sigma is unchanged. *)
-        let (gl, _) = Goal.eval nf_enter_t env sigma goal in
-        Some gl
-    in
-    tclUNIT (List.map_filter map step.comb)
-
   let goals =
     Proof.current >>= fun env ->
     Proof.get >>= fun step ->
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 94969f3a5c..bda88178bf 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -395,6 +395,9 @@ module Goal : sig
   (** Assume that you do not need the goal to be normalized. *)
   val assume : 'a t -> [ `NF ] t
 
+  (** Normalises the argument goal. *)
+  val normalize : 'a t -> [ `NF ] t tactic
+
   (* [concl], [hyps], [env] and [sigma] given a goal [gl] return
      respectively the conclusion of [gl], the hypotheses of [gl], the
      environment of [gl] (i.e. the global environment and the hypotheses)
@@ -412,9 +415,6 @@ module Goal : sig
   (** Same as nf_enter, but does not normalize the goal beforehand. *)
   val enter : ([ `LZ ] t -> unit tactic) -> unit tactic
 
-  (** Recover the list of current goals under focus *)
-  val nf_goals : [ `NF ] t list tactic
-
   (** Recover the list of current goals under focus, without evar-normalization *)
   val goals : [ `LZ ] t list tactic
 
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))