diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 8 | ||||
| -rw-r--r-- | tactics/auto.mli | 4 |
2 files changed, 6 insertions, 6 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index b51da4fe0..fa1985d8c 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 69568d4f8..b6bb5365c 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 |