From 329dcbec0e950f58334ec46938d7d74ad73cb617 Mon Sep 17 00:00:00 2001
From: jforest
Date: Sat, 8 Mar 2008 16:05:33 +0000
Subject: correction d'un bug d'efficacite dans Function (+ ajout de
 eauto_with_bases)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10640 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/eauto.ml4 | 7 +++++--
 tactics/eauto.mli | 6 ++++++
 2 files changed, 11 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 706ba98401..ab62aa9cf5 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -365,7 +365,10 @@ let e_search_auto debug (in_depth,p) lems db_list gl =
 
 open Evd
 
-let eauto debug np lems dbnames =
+let eauto_with_bases debug np lems db_list = 
+  tclTRY (e_search_auto debug np lems db_list)
+
+let eauto debug np lems dbnames = 
   let db_list =
     List.map
       (fun x -> 
@@ -374,7 +377,7 @@ let eauto debug np lems dbnames =
       ("core"::dbnames) 
   in
   tclTRY (e_search_auto debug np lems db_list)
-
+  
 let full_eauto debug n lems gl = 
   let dbnames = current_db_names () in
   let dbnames =  list_subtract dbnames ["v62"] in
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index 34655b1341..d1883aa664 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -29,3 +29,9 @@ val e_give_exact_constr : constr -> tactic
 
 val gen_eauto : bool -> bool * int -> constr list -> 
   hint_db_name list option -> tactic
+
+
+val eauto_with_bases :
+  bool ->
+  bool * int ->
+  Term.constr list -> Auto.Hint_db.t list -> Proof_type.tactic
-- 
cgit v1.2.3