diff options
| author | Maxime Dénès | 2019-04-24 21:10:30 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-02 12:28:19 +0200 |
| commit | ef0ef9f318a0af6542835b71ce7aaced021fff6d (patch) | |
| tree | 93d8ad8e76b785a90bf891a6c52fecf592b8a6de /tactics/class_tactics.mli | |
| parent | 213b5419136e4639f345e171c086b154c14aa62c (diff) | |
Document typeclasses_eauto
Diffstat (limited to 'tactics/class_tactics.mli')
| -rw-r--r-- | tactics/class_tactics.mli | 15 |
1 files changed, 12 insertions, 3 deletions
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 |