From 4b29ca791bdfc810feabb883dc3d96a4ebd130a1 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <mattam@mattam.org>
Date: Thu, 9 Jun 2016 21:48:30 +0200
Subject: Purely refactoring and code/API cleanup.

Fix test-suite files
---
 tactics/class_tactics.mli | 41 +++++++++++++++++------------------------
 1 file changed, 17 insertions(+), 24 deletions(-)

(limited to 'tactics/class_tactics.mli')

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
-- 
cgit v1.2.3