Merge branch 'master'.

1 files changed, 9 insertions, 1 deletions

diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli
index 8855093ee..a38be5972 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -21,7 +21,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
 
@@ -37,8 +41,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 ->