diff options
author | Matthieu Sozeau <mattam@mattam.org> | 2016-06-09 21:48:30 +0200 |
---|---|---|
committer | Matthieu Sozeau <mattam@mattam.org> | 2016-06-16 18:21:08 +0200 |
commit | 4b29ca791bdfc810feabb883dc3d96a4ebd130a1 (patch) | |
tree | 0e0825576f6e02fd3d997ee4374dca5cd934226d /tactics/class_tactics.mli | |
parent | 6876a3cd9dd1d7c94f9d387904c6a6f6d88c31f8 (diff) |
Purely refactoring and code/API cleanup.
Fix test-suite files
Diffstat (limited to 'tactics/class_tactics.mli')
-rw-r--r-- | tactics/class_tactics.mli | 41 |
1 files changed, 17 insertions, 24 deletions
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli index 48abba1aa..2fb0bbb04 100644 --- a/tactics/class_tactics.mli +++ b/tactics/class_tactics.mli @@ -20,10 +20,9 @@ val get_typeclasses_debug : unit -> bool val set_typeclasses_depth : int option -> unit val get_typeclasses_depth : unit -> int option -val progress_evars : unit Proofview.tactic -> unit Proofview.tactic - val typeclasses_eauto : ?only_classes:bool -> ?st:transparent_state -> - Hints.hint_db_name list -> unit Proofview.tactic + depth:(Int.t option) -> + Hints.hint_db_name list -> unit Proofview.tactic val head_of_constr : Id.t -> Term.constr -> unit Proofview.tactic @@ -33,24 +32,18 @@ val is_ground : constr -> tactic val autoapply : constr -> Hints.hint_db_name -> tactic -type newautoinfo = - { search_depth : int list; - last_tac : Pp.std_ppcmds Lazy.t; - search_dep : bool; - search_cut : Hints.hints_path; - search_hints : Hints.Hint_db.t } - -val new_hints_tac : bool -> Hints.hint_db list -> - newautoinfo -> - (newautoinfo -> unit Proofview.tactic) -> unit Proofview.tactic - -val make_autogoal' : ?st:Names.transparent_state -> - bool -> bool -> - Hints.hints_path -> int -> ([ `NF ], 'c) Proofview.Goal.t -> newautoinfo - -val new_eauto_tac : ?st:Names.transparent_state -> - bool -> ?limit:Int.t -> - bool -> (* Should the tactic be made backtracking, whatever the dependencies - betwwen initial goals are *) - Hints.hint_db list -> unit Proofview.tactic - +module Search : sig + val eauto_tac : + ?st:Names.transparent_state -> + (** The transparent_state used when working with local hypotheses *) + only_classes:bool -> + (** Should non-class goals be shelved and resolved at the end *) + depth:Int.t option -> + (** Bounded or unbounded search *) + dep:bool -> + (** Should the tactic be made backtracking on the initial goals, + whatever their internal dependencies are. *) + Hints.hint_db list -> + (** The list of hint databases to use *) + unit Proofview.tactic +end |