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

1 files 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 *)