From 2aa939230dde070c5cf20f01a49cb0891e2027e4 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 20 Apr 2011 10:27:28 +0000
Subject: This is used in the rippling plugin. This also allows fixing bug
 #2188.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14030 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/auto.ml  | 8 ++++----
 tactics/auto.mli | 4 ++--
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/tactics/auto.ml b/tactics/auto.ml
index b51da4fe08..fa1985d8c5 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -1140,7 +1140,7 @@ let search = search_gen 0
 
 let default_search_depth = ref 5
 
-let delta_auto mod_delta n lems dbnames gl =
+let delta_auto ?(use_core_db=true) mod_delta n lems dbnames gl =
   let db_list =
     List.map
       (fun x ->
@@ -1148,13 +1148,13 @@ let delta_auto mod_delta n lems dbnames gl =
 	   searchtable_map x
 	 with Not_found ->
 	   error_no_such_hint_database x)
-      ("core"::dbnames)
+      (if use_core_db then "core"::dbnames else dbnames)
   in
   tclTRY (search n mod_delta db_list (make_local_hint_db false lems gl)) gl
 
-let auto = delta_auto false
+let auto ?(use_core_db=true) = delta_auto ~use_core_db false
 
-let new_auto = delta_auto true
+let new_auto ?(use_core_db=true) = delta_auto ~use_core_db true
 
 let default_auto = auto !default_search_depth [] []
 
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 69568d4f8d..b6bb5365cf 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -192,11 +192,11 @@ val conclPattern : constr -> constr_pattern option -> Tacexpr.glob_tactic_expr -
 
 (** The Auto tactic *)
 
-val auto : int -> open_constr list -> hint_db_name list -> tactic
+val auto : ?use_core_db:bool -> int -> open_constr list -> hint_db_name list -> tactic
 
 (** Auto with more delta. *)
 
-val new_auto : int -> open_constr list -> hint_db_name list -> tactic
+val new_auto : ?use_core_db:bool -> int -> open_constr list -> hint_db_name list -> tactic
 
 (** auto with default search depth and with the hint database "core" *)
 val default_auto : tactic
-- 
cgit v1.2.3