summaryrefslogtreecommitdiff
path: root/tactics/auto.mli
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/auto.mli')
-rw-r--r--tactics/auto.mli43
1 files changed, 30 insertions, 13 deletions
diff --git a/tactics/auto.mli b/tactics/auto.mli
index ecd20f0d..37406a30 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: auto.mli 7937 2006-01-28 19:58:11Z herbelin $ i*)
+(*i $Id: auto.mli 10868 2008-04-29 12:30:25Z msozeau $ i*)
(*i*)
open Util
@@ -58,10 +58,14 @@ module Hint_db :
type hint_db_name = string
-val searchtable_map : hint_db_name -> Hint_db.t
+type hint_db = transparent_state * Hint_db.t
+
+val searchtable_map : hint_db_name -> hint_db
val current_db_names : unit -> hint_db_name list
+val add_hint_list : (global_reference * pri_auto_tactic) list -> hint_db -> hint_db
+
val add_hints : locality_flag -> hint_db_name list -> hints -> unit
val print_searchtable : unit -> unit
@@ -72,19 +76,19 @@ val print_hint_ref : global_reference -> unit
val print_hint_db_by_name : hint_db_name -> unit
-(* [make_exact_entry hint_name (c, ctyp)].
+(* [make_exact_entry pri (c, ctyp)].
[c] is the term given as an exact proof to solve the goal;
- [ctyp] is the type of [hc]. *)
+ [ctyp] is the type of [c]. *)
-val make_exact_entry : constr * constr -> global_reference * pri_auto_tactic
+val make_exact_entry : int option -> constr * constr -> global_reference * pri_auto_tactic
-(* [make_apply_entry (eapply,verbose) (c,cty)].
+(* [make_apply_entry (eapply,verbose) pri (c,cty)].
[eapply] is true if this hint will be used only with EApply;
[c] is the term given as an exact proof to solve the goal;
[cty] is the type of [hc]. *)
val make_apply_entry :
- env -> evar_map -> bool * bool -> constr * constr
+ env -> evar_map -> bool * bool -> int option -> constr * constr
-> global_reference * pri_auto_tactic
(* A constr which is Hint'ed will be:
@@ -95,7 +99,7 @@ val make_apply_entry :
has missing arguments. *)
val make_resolves :
- env -> evar_map -> bool -> constr ->
+ env -> evar_map -> bool * bool -> int option -> constr ->
(global_reference * pri_auto_tactic) list
(* [make_resolve_hyp hname htyp].
@@ -125,16 +129,21 @@ val set_extern_subst_tactic :
-> unit
(* Create a Hint database from the pairs (name, constr).
- Useful to take the current goal hypotheses as hints *)
+ Useful to take the current goal hypotheses as hints;
+ Boolean tells if lemmas with evars are allowed *)
-val make_local_hint_db : constr list -> goal sigma -> Hint_db.t
+val make_local_hint_db : bool -> constr list -> goal sigma -> hint_db
val priority : (int * 'a) list -> 'a list
val default_search_depth : int ref
+val auto_unif_flags : Unification.unify_flags
+
(* Try unification with the precompiled clause, then use registered Apply *)
-val unify_resolve : (constr * clausenv) -> tactic
+val unify_resolve_nodelta : (constr * clausenv) -> tactic
+
+val unify_resolve : Unification.unify_flags -> (constr * clausenv) -> tactic
(* [ConclPattern concl pat tacast]:
if the term concl matches the pattern pat, (in sense of
@@ -147,12 +156,20 @@ val conclPattern : constr -> constr_pattern -> Tacexpr.glob_tactic_expr -> tacti
val auto : int -> constr list -> hint_db_name list -> tactic
+(* Auto with more delta. *)
+
+val new_auto : int -> 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 -> constr list -> tactic
+(* auto with all hint databases except the "v62" compatibility database
+ and doing delta *)
+val new_full_auto : int -> constr list -> tactic
+
(* auto with default search depth and with all hint databases
except the "v62" compatibility database *)
val default_full_auto : tactic
@@ -174,11 +191,11 @@ val fmt_autotactic : auto_tactic -> Pp.std_ppcmds
(*s The following is not yet up to date -- Papageno. *)
(* DAuto *)
-val dauto : int option * int option -> tactic
+val dauto : int option * int option -> constr list -> tactic
val default_search_decomp : int ref
val default_dauto : tactic
-val h_dauto : int option * int option -> tactic
+val h_dauto : int option * int option -> constr list -> tactic
(* SuperAuto *)
type autoArguments =