From 9cdadde0422382852eddefa17201778606256f2f Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Sat, 2 Nov 2013 15:39:57 +0000
Subject: Corrects a bug on Proofview.Goal.enter whereby sigmas were captured
 and used at the wrong time.

The bug was masked by the fact that Tacinterp uses many superfluous Proofview.Goal.enter, it so happens that the tactic
Proofview.Goal.enter (fun _ -> Proofview.Goal.enter fun gl -> t))
had the correct semantics!

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17014 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/proofview.ml | 27 ++++++++++++++++++++++-----
 1 file changed, 22 insertions(+), 5 deletions(-)

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 5e1e1e6a4d..40b9c0f8a4 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -748,12 +748,29 @@ module Goal = struct
     f {env=env;sigma=sigma;hyps=hyps;concl=concl;self=self}
   end
   let enter f =
-    lift (enter_t f) >= fun ts ->
-    tclDISPATCH ts
+    list_iter_goal () begin fun goal () ->
+      Proof.current >= fun env ->
+      tclEVARMAP >= fun sigma ->
+      try
+        (* enter_t cannot modify the sigma. *)
+        let (t,_) = Goal.eval (enter_t f) env sigma goal in
+        t
+      with e when catchable_exception e ->
+        tclZERO e
+    end
   let enterl f =
-    lift (enter_t f) >= fun ts ->
-    tclDISPATCHL ts >= fun res ->
-    tclUNIT (List.flatten res)
+    list_iter_goal [] begin fun goal acc ->
+      Proof.current >= fun env ->
+      tclEVARMAP >= fun sigma ->
+      try
+        (* enter_t cannot modify the sigma. *)
+        let (t,_) = Goal.eval (enter_t f) env sigma goal in
+        t >= fun r ->
+        tclUNIT (r::acc)
+      with e when catchable_exception e ->
+        tclZERO e
+    end >= fun res ->
+    tclUNIT (List.flatten (List.rev res))
 
 
   (* compatibility *)
-- 
cgit v1.2.3