diff options
Diffstat (limited to 'tactics/auto.mli')
| -rw-r--r-- | tactics/auto.mli | 37 |
1 files changed, 25 insertions, 12 deletions
diff --git a/tactics/auto.mli b/tactics/auto.mli index 95de089e0..69a526e5a 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -219,48 +219,61 @@ val conclPattern : constr -> constr_pattern option -> Tacexpr.glob_tactic_expr - val make_db_list : hint_db_name list -> hint_db list -val auto : int -> open_constr list -> hint_db_name list -> tactic +val auto : ?debug:Tacexpr.debug -> + 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 : ?debug:Tacexpr.debug -> + int -> open_constr list -> hint_db_name list -> tactic (** auto with default search depth and with the hint database "core" *) val default_auto : tactic (** auto with all hint databases except the "v62" compatibility database *) -val full_auto : int -> open_constr list -> tactic +val full_auto : ?debug:Tacexpr.debug -> + int -> open_constr list -> tactic (** auto with all hint databases except the "v62" compatibility database and doing delta *) -val new_full_auto : int -> open_constr list -> tactic +val new_full_auto : ?debug:Tacexpr.debug -> + int -> open_constr list -> tactic (** auto with default search depth and with all hint databases except the "v62" compatibility database *) val default_full_auto : tactic (** The generic form of auto (second arg [None] means all bases) *) -val gen_auto : int option -> open_constr list -> hint_db_name list option -> tactic +val gen_auto : ?debug:Tacexpr.debug -> + int option -> open_constr list -> hint_db_name list option -> tactic (** The hidden version of auto *) -val h_auto : int option -> open_constr list -> hint_db_name list option -> tactic +val h_auto : ?debug:Tacexpr.debug -> + int option -> open_constr list -> hint_db_name list option -> tactic (** Trivial *) -val trivial : open_constr list -> hint_db_name list -> tactic -val gen_trivial : open_constr list -> hint_db_name list option -> tactic -val full_trivial : open_constr list -> tactic -val h_trivial : open_constr list -> hint_db_name list option -> tactic + +val trivial : ?debug:Tacexpr.debug -> + open_constr list -> hint_db_name list -> tactic +val gen_trivial : ?debug:Tacexpr.debug -> + open_constr list -> hint_db_name list option -> tactic +val full_trivial : ?debug:Tacexpr.debug -> + open_constr list -> tactic +val h_trivial : ?debug:Tacexpr.debug -> + open_constr list -> hint_db_name list option -> tactic val pr_autotactic : 'a auto_tactic -> Pp.std_ppcmds (** Destructing Auto *) (** DAuto *) -val dauto : int option * int option -> open_constr list -> tactic +val dauto : ?debug:Tacexpr.debug -> + int option * int option -> open_constr list -> tactic val default_search_decomp : int ref val default_dauto : tactic -val h_dauto : int option * int option -> open_constr list -> tactic +val h_dauto : ?debug:Tacexpr.debug -> + int option * int option -> open_constr list -> tactic (** Hook for changing the initialization of auto *) |