From 1e6c3e993fd33d01713aae34a8cefbc210b3898a Mon Sep 17 00:00:00 2001
From: barras
Date: Fri, 15 Feb 2002 18:02:05 +0000
Subject: petits changements cosmetiques sur les tactiques + Clear independant
 de l'ordre des hypotheses, et substituant les hypotheses definies

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2481 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/interface/blast.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'contrib/interface')

diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index 102135e96d..f6a47f9862 100755
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -465,7 +465,7 @@ let rec search_gen decomp n db_list local_db extra_sign goal =
 	(List.map 
 	   (fun id -> tclTHEN (decomp_unary_term (mkVar id)) 
 		(tclTHEN 
-		   (clear_one id)
+		   (clear [id])
 		   (free_try (search_gen decomp p db_list local_db []))))
 	   (pf_ids_of_hyps goal)) 
   in
-- 
cgit v1.2.3