diff options
| author | msozeau | 2011-04-20 10:27:28 +0000 |
|---|---|---|
| committer | msozeau | 2011-04-20 10:27:28 +0000 |
| commit | 2aa939230dde070c5cf20f01a49cb0891e2027e4 (patch) | |
| tree | 79bfc8f2ba7cb1e7531d3ff0e34c425463f50953 /tactics/auto.ml | |
| 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/auto.ml')
| -rw-r--r-- | tactics/auto.ml | 8 |
1 files changed, 4 insertions, 4 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 [] [] |