From ef0ef9f318a0af6542835b71ce7aaced021fff6d Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 24 Apr 2019 21:10:30 +0200
Subject: Document typeclasses_eauto

---
 tactics/class_tactics.mli | 15 ++++++++++++---
 1 file changed, 12 insertions(+), 3 deletions(-)

(limited to 'tactics')

diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli
index c950e3de3d..2d8b07b083 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -27,9 +27,18 @@ type search_strategy = Dfs | Bfs
 
 val set_typeclasses_strategy : search_strategy -> unit
 
-val typeclasses_eauto : ?only_classes:bool -> ?st:TransparentState.t -> ?strategy:search_strategy ->
-                        depth:(Int.t option) ->
-                        Hints.hint_db_name list -> unit Proofview.tactic
+val typeclasses_eauto :
+  ?only_classes:bool
+  (** Should non-class goals be shelved and resolved at the end *)
+  -> ?st:TransparentState.t
+  (** The transparent_state used when working with local hypotheses  *)
+  -> ?strategy:search_strategy
+  (** Is a traversing-strategy specified? *)
+  -> depth:(Int.t option)
+  (** Bounded or unbounded search *)
+  -> Hints.hint_db_name list
+  (** The list of hint databases to use *)
+  -> unit Proofview.tactic
 
 val head_of_constr : Id.t -> constr -> unit Proofview.tactic
 
-- 
cgit v1.2.3