From 892c74d099fd9eda1e2f179645f7e1d9b67ba49b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 18 Sep 2014 17:18:34 +0200
Subject: Fixing strange evarmap leak in goals.

Goals have to be refreshed when observed, because the evarmap may have
changed between the moment where the goal was generated and the moment the
goal is used.
---
 proofs/proofview.ml  | 8 ++++++--
 proofs/proofview.mli | 2 +-
 tactics/ftactic.ml   | 3 ++-
 3 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 75725e47c4..6ecf4da7e6 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -942,8 +942,12 @@ module Goal = struct
       match Goal.advance sigma goal with
       | None -> None (** ppedrot: Is this check really necessary? *)
       | Some goal ->
-        (** The sigma is unchanged. *)
-        let (gl, _) = Goal.eval (enter_t (fun gl -> gl)) env sigma goal in
+        let gl =
+          tclEVARMAP >>= fun sigma ->
+          (** The sigma is unchanged. *)
+          let (gl, _) = Goal.eval (enter_t (fun gl -> gl)) env sigma goal in
+          tclUNIT gl
+        in
         Some gl
     in
     tclUNIT (List.map_filter map step.comb)
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index bda88178bf..c44707c1e7 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -416,7 +416,7 @@ module Goal : sig
   val enter : ([ `LZ ] t -> unit tactic) -> unit tactic
 
   (** Recover the list of current goals under focus, without evar-normalization *)
-  val goals : [ `LZ ] t list tactic
+  val goals : [ `LZ ] t tactic list tactic
 
   (* compatibility: avoid if possible *)
   val goal : [ `NF ] t -> Goal.goal
diff --git a/tactics/ftactic.ml b/tactics/ftactic.ml
index 43602d1fb6..d8b12fc4e4 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))
-- 
cgit v1.2.3