diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-20 10:27:28 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-20 10:27:28 +0000 |
| commit | 2aa939230dde070c5cf20f01a49cb0891e2027e4 (patch) | |
| tree | 79bfc8f2ba7cb1e7531d3ff0e34c425463f50953 /tactics | |
| parent | cf35c36c341d7f1f615b3e11e6aab64a7fa6a5bf (diff) | |
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
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 |