Auto: removal of ?use_core_db obsolete now that we have nocore

 Suggestion of Tom Prince, that told me that he has adapted the rippling
 tactic to use the "nocore" pseudo-database. Since this tactic was the
 only user of these optional arguments ?use_core_db, let's remove them.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14629 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 13 insertions, 17 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 72917530b2..db2524c30f 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -1063,13 +1063,11 @@ and trivial_resolve mod_delta db_list local_db cl =
 	    (my_find_search mod_delta db_list local_db head cl))
   with Not_found -> []
 
-(** Two ways to disable the use of the "core" database:
-    - Via the optional argument : use_core_db=false
-      This is kept for compatibility with the rippling plugin.
-    - By passing "nocore" amongst the databases *)
+(** The use of the "core" database can be de-activated by passing
+    "nocore" amongst the databases. *)
 
-let make_db_list ?(use_core_db=true) dbnames =
-  let use_core = use_core_db && not (List.mem "nocore" dbnames) in
+let make_db_list dbnames =
+  let use_core = not (List.mem "nocore" dbnames) in
   let dbnames = list_remove "nocore" dbnames in
   let dbnames = if use_core then "core"::dbnames else dbnames in
   let lookup db =
@@ -1184,13 +1182,13 @@ let search = search_gen 0
 
 let default_search_depth = ref 5
 
-let delta_auto ?(use_core_db=true) mod_delta n lems dbnames gl =
-  let db_list = make_db_list ~use_core_db dbnames in
+let delta_auto mod_delta n lems dbnames gl =
+  let db_list = make_db_list dbnames in
   tclTRY (search n mod_delta db_list (make_local_hint_db false lems gl)) gl
 
-let auto ?(use_core_db=true) = delta_auto ~use_core_db false
+let auto = delta_auto false
 
-let new_auto ?(use_core_db=true) = delta_auto ~use_core_db true
+let new_auto = delta_auto true
 
 let default_auto = auto !default_search_depth [] []
 
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 1bff2eef85..ce2b33013b 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -194,18 +194,16 @@ val conclPattern : constr -> constr_pattern option -> Tacexpr.glob_tactic_expr -
 
 (** The Auto tactic *)
 
-(** Two ways to disable the use of the "core" database:
-    - Via the optional argument : use_core_db=false
-      This is kept for compatibility with the rippling plugin.
-    - By passing "nocore" amongst the databases *)
+(** The use of the "core" database can be de-activated by passing
+    "nocore" amongst the databases. *)
 
-val make_db_list : ?use_core_db:bool -> hint_db_name list -> hint_db list
+val make_db_list : hint_db_name list -> hint_db list
 
-val auto : ?use_core_db:bool -> int -> open_constr list -> hint_db_name list -> tactic
+val auto : int -> open_constr list -> hint_db_name list -> tactic
 
 (** Auto with more delta. *)
 
-val new_auto : ?use_core_db:bool -> int -> open_constr list -> hint_db_name list -> tactic
+val new_auto : int -> open_constr list -> hint_db_name list -> tactic
 
 (** auto with default search depth and with the hint database "core" *)
 val default_auto : tactic