From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 25 Jul 2008 15:12:53 +0200
Subject: Imported Upstream version 8.2~beta3+dfsg

---
 tactics/auto.mli | 43 ++++++++++++++++++++++++++++++-------------
 1 file changed, 30 insertions(+), 13 deletions(-)

(limited to 'tactics/auto.mli')

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 =
-- 
cgit v1.2.3