diff options
author | Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
commit | 870075f34dd9fa5792bfbf413afd3b96f17e76a0 (patch) | |
tree | 0c647056de1832cf1dba5ba58758b9121418e4be /tactics/auto.mli | |
parent | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (diff) |
Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg
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 |