diff options
Diffstat (limited to 'tactics/class_tactics.mli')
| -rw-r--r-- | tactics/class_tactics.mli | 31 |
1 files changed, 28 insertions, 3 deletions
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli index f1bcfa7d..76760db0 100644 --- a/tactics/class_tactics.mli +++ b/tactics/class_tactics.mli @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** This files implements typeclasses eauto *) + open Names open Constr open Tacmach @@ -18,10 +20,13 @@ 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 +type search_strategy = Dfs | Bfs + +val set_typeclasses_strategy : search_strategy -> unit -val typeclasses_eauto : ?only_classes:bool -> ?st:transparent_state -> - Hints.hint_db_name list -> tactic +val typeclasses_eauto : ?only_classes:bool -> ?st:transparent_state -> ?strategy:search_strategy -> + depth:(Int.t option) -> + Hints.hint_db_name list -> unit Proofview.tactic val head_of_constr : Id.t -> Term.constr -> unit Proofview.tactic @@ -30,3 +35,23 @@ val not_evar : constr -> unit Proofview.tactic val is_ground : constr -> tactic val autoapply : constr -> Hints.hint_db_name -> tactic + +module Search : sig + val eauto_tac : + ?st:Names.transparent_state -> + (** The transparent_state used when working with local hypotheses *) + ?unique:bool -> + (** Should we force a unique solution *) + only_classes:bool -> + (** Should non-class goals be shelved and resolved at the end *) + ?strategy:search_strategy -> + (** Is a traversing-strategy specified? *) + 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 |