diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-04 17:44:41 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-04 17:44:41 +0000 |
| commit | f06c30e82609e4d09fb2103a19ef501024251c6c (patch) | |
| tree | 0b77a88f39013269ee33526140882f5154f27e5b /tactics/auto.mli | |
| parent | 4b1656d0931209ac07660bebbf22d43d67581dee (diff) | |
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
Diffstat (limited to 'tactics/auto.mli')
| -rw-r--r-- | tactics/auto.mli | 12 |
1 files changed, 5 insertions, 7 deletions
diff --git a/tactics/auto.mli b/tactics/auto.mli index 1bff2eef8..ce2b33013 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 |