From d445ad43b174c98c49927814fb6f48b2efff49cc Mon Sep 17 00:00:00 2001
From: delahaye
Date: Fri, 31 May 2002 21:08:10 +0000
Subject: Les VContext ne sont plus des fermetures (temporaire)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2743 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tacinterp.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 9895f955dc..e0a573d642 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1389,7 +1389,9 @@ and vcontext_interp ist = function
   | (VContext (ist',lr,lmr)) as v ->
     (match ist.goalopt with
     | None -> v
-    | Some g -> (* Relaunch *) match_context_interp ist' lr lmr g)
+    | 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)*)
   | v -> v
 
 (* Tries to match the hypotheses in a Match Context *)
-- 
cgit v1.2.3