Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg

1 files changed, 31 insertions, 21 deletions

diff --git a/tactics/auto.mli b/tactics/auto.mli
index edaaa1c1..c9065ef3 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 11282 2008-07-28 11:51:53Z msozeau $ i*)
+(*i $Id: auto.mli 11735 2009-01-02 17:22:31Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -44,20 +44,24 @@ type stored_data = pri_auto_tactic
 
 type search_entry = stored_data list * stored_data list * stored_data Btermdn.t
 
+(* The head may not be bound. *)
+
+type hint_entry = global_reference option * pri_auto_tactic
+
 module Hint_db :
   sig
     type t
-    val empty : bool -> t
+    val empty : transparent_state -> bool -> t
     val find : global_reference -> t -> search_entry
     val map_all : global_reference -> t -> pri_auto_tactic list
     val map_auto : global_reference * constr -> t -> pri_auto_tactic list
-    val add_one : global_reference * pri_auto_tactic -> t -> t
-    val add_list : (global_reference * pri_auto_tactic) list -> t -> t
-    val iter : (global_reference -> stored_data list -> unit) -> t -> unit
+    val add_one : hint_entry -> t -> t
+    val add_list : (hint_entry) list -> t -> t
+    val iter : (global_reference option -> stored_data list -> unit) -> t -> unit
 
+    val use_dn : t -> bool
     val transparent_state : t -> transparent_state
     val set_transparent_state : t -> transparent_state -> t
-    val set_rigid : t -> constant -> t
   end
 
 type hint_db_name = string
@@ -68,7 +72,12 @@ val searchtable_map : hint_db_name -> hint_db
 
 val searchtable_add : (hint_db_name * hint_db) -> unit
 
-val create_hint_db : bool -> hint_db_name -> bool -> unit
+(* [create_hint_db local name st use_dn]. 
+   [st] is a transparency state for unification using this db
+   [use_dn] switches the use of the discrimination net for all hints 
+   and patterns. *)
+
+val create_hint_db : bool -> hint_db_name -> transparent_state -> bool -> unit
 
 val current_db_names : unit -> hint_db_name list
 
@@ -86,16 +95,18 @@ val print_hint_db_by_name : hint_db_name -> unit
    [c] is the term given as an exact proof to solve the goal;
    [ctyp] is the type of [c]. *)
 
-val make_exact_entry : int option -> constr * constr -> global_reference * pri_auto_tactic
+val make_exact_entry : int option -> constr * constr -> hint_entry
 
 (* [make_apply_entry (eapply,verbose) pri (c,cty)].
    [eapply] is true if this hint will be used only with EApply;
+   [hnf] should be true if we should expand the head of cty before searching for 
+   products;
    [c] is the term given as an exact proof to solve the goal;
-   [cty] is the type of [hc]. *)
-
+   [cty] is the type of [c]. *)
+  
 val make_apply_entry :
-  env -> evar_map -> bool * bool -> int option -> constr * constr
-      -> global_reference * pri_auto_tactic
+  env -> evar_map -> bool * bool * bool -> int option -> constr * constr
+      -> hint_entry
 
 (* A constr which is Hint'ed will be:
    (1) used as an Exact, if it does not start with a product
@@ -105,8 +116,8 @@ val make_apply_entry :
        has missing arguments. *)
 
 val make_resolves :
-  env -> evar_map -> bool * bool -> int option -> constr -> 
-      (global_reference * pri_auto_tactic) list
+  env -> evar_map -> bool * bool * bool -> int option -> constr -> 
+      hint_entry list
 
 (* [make_resolve_hyp hname htyp].
    used to add an hypothesis to the local hint database;
@@ -114,14 +125,13 @@ val make_resolves :
    If the hyp cannot be used as a Hint, the empty list is returned. *)
 
 val make_resolve_hyp : 
-  env -> evar_map -> named_declaration ->
-      (global_reference * pri_auto_tactic) list
+  env -> evar_map -> named_declaration -> hint_entry list
 
 (* [make_extern pri pattern tactic_expr] *)
 
 val make_extern :
-  int -> constr_pattern -> Tacexpr.glob_tactic_expr
-      -> global_reference * pri_auto_tactic
+  int -> constr_pattern option -> Tacexpr.glob_tactic_expr
+      -> hint_entry
 
 val set_extern_interp :
   (patvar_map -> Tacexpr.glob_tactic_expr -> tactic) -> unit
@@ -140,7 +150,7 @@ val set_extern_subst_tactic :
 
 val make_local_hint_db : bool -> constr list -> goal sigma -> hint_db
 
-val priority : (int * 'a) list -> 'a list
+val priority : ('a * pri_auto_tactic) list -> ('a * pri_auto_tactic) list
 
 val default_search_depth : int ref
 
@@ -156,7 +166,7 @@ val unify_resolve : Unification.unify_flags -> (constr * clausenv) -> tactic
    [Pattern.somatches], then replace [?1] [?2] metavars in tacast by the
    right values to build a tactic *)
 
-val conclPattern : constr -> constr_pattern -> Tacexpr.glob_tactic_expr -> tactic
+val conclPattern : constr -> constr_pattern option -> Tacexpr.glob_tactic_expr -> tactic
 
 (* The Auto tactic *)
 
@@ -192,7 +202,7 @@ val gen_trivial : constr list -> hint_db_name list option -> tactic
 val full_trivial : constr list -> tactic
 val h_trivial : constr list -> hint_db_name list option -> tactic
 
-val fmt_autotactic : auto_tactic -> Pp.std_ppcmds
+val pr_autotactic : auto_tactic -> Pp.std_ppcmds
 
 (*s The following is not yet up to date -- Papageno. *)