From f32f5b2c989adcf195348589420a9b8635f845b9 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 13 Jun 2002 16:18:09 +0000
Subject: 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
---
 tactics/tacinterp.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 9609bb49f9..99ed8aeb1a 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 *)
-- 
cgit v1.2.3