diff options
Diffstat (limited to 'tactics/class_tactics.mli')
| -rw-r--r-- | tactics/class_tactics.mli | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli index 8db264ad9..76760db02 100644 --- a/tactics/class_tactics.mli +++ b/tactics/class_tactics.mli @@ -20,7 +20,11 @@ val get_typeclasses_debug : unit -> bool val set_typeclasses_depth : int option -> unit val get_typeclasses_depth : unit -> int option -val typeclasses_eauto : ?only_classes:bool -> ?st:transparent_state -> +type search_strategy = Dfs | Bfs + +val set_typeclasses_strategy : search_strategy -> unit + +val typeclasses_eauto : ?only_classes:bool -> ?st:transparent_state -> ?strategy:search_strategy -> depth:(Int.t option) -> Hints.hint_db_name list -> unit Proofview.tactic @@ -36,8 +40,12 @@ 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 -> |