Réparation de l'interprétation des fermetures (sans casser Field!)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2779 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 3 insertions, 4 deletions

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 9609bb49f..99ed8aeb1 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1386,10 +1386,9 @@ and vcontext_interp ist = function
   | (VContext (ist',lr,lmr)) as v ->
     (match ist.goalopt with
     | None -> v
-    | Some g ->
-        match_context_interp ist lr lmr g)
-(* The closure system does not work yet. It must be better studied. *)
-(* (* Relaunch *) match_context_interp ist' lr lmr g)*)
+    | Some g as go -> 
+        let ist = { ist' with goalopt = go; env = pf_env g; evc = project g }
+        in match_context_interp ist lr lmr g)
   | v -> v
 
 (* Tries to match the hypotheses in a Match Context *)