diff options
Diffstat (limited to 'tactics/auto.mli')
| -rw-r--r-- | tactics/auto.mli | 18 |
1 files changed, 13 insertions, 5 deletions
diff --git a/tactics/auto.mli b/tactics/auto.mli index 37406a30..edaaa1c1 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 10868 2008-04-29 12:30:25Z msozeau $ i*) +(*i $Id: auto.mli 11282 2008-07-28 11:51:53Z msozeau $ i*) (*i*) open Util @@ -47,24 +47,30 @@ type search_entry = stored_data list * stored_data list * stored_data Btermdn.t module Hint_db : sig type t - val empty : t + val empty : 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 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 -type hint_db = transparent_state * Hint_db.t +type hint_db = Hint_db.t val searchtable_map : hint_db_name -> hint_db -val current_db_names : unit -> hint_db_name list +val searchtable_add : (hint_db_name * hint_db) -> unit -val add_hint_list : (global_reference * pri_auto_tactic) list -> hint_db -> hint_db +val create_hint_db : bool -> hint_db_name -> bool -> unit + +val current_db_names : unit -> hint_db_name list val add_hints : locality_flag -> hint_db_name list -> hints -> unit @@ -207,3 +213,5 @@ val superauto : int -> (identifier * constr) list -> autoArguments list -> tacti *) val h_superauto : int option -> reference list -> bool -> bool -> tactic + +val auto_init : (unit -> unit) ref |