summaryrefslogtreecommitdiff
path: root/tactics/auto.mli
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/auto.mli')
-rw-r--r--tactics/auto.mli54
1 files changed, 22 insertions, 32 deletions
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 521c5ed2..87786e5b 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -102,8 +102,6 @@ type hints_entry =
| HintsTransparencyEntry of evaluable_global_reference list * bool
| HintsExternEntry of
int * (patvar list * constr_pattern) option * Tacexpr.glob_tactic_expr
- | HintsDestructEntry of identifier * int * (bool,unit) Tacexpr.location *
- (patvar list * constr_pattern) * Tacexpr.glob_tactic_expr
val searchtable_map : hint_db_name -> hint_db
@@ -220,59 +218,51 @@ 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 pr_autotactic : 'a auto_tactic -> Pp.std_ppcmds
-
-(** {6 The following is not yet up to date -- Papageno. } *)
-
-(** DAuto *)
-val dauto : 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 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
-(** SuperAuto *)
-
-type autoArguments =
- | UsingTDB
- | Destructing
-
-(*
-val superauto : int -> (identifier * constr) list -> autoArguments list -> tactic
-*)
+val pr_autotactic : 'a auto_tactic -> Pp.std_ppcmds
-val h_superauto : int option -> reference list -> bool -> bool -> tactic
+(** Hook for changing the initialization of auto *)
val add_auto_init : (unit -> unit) -> unit