diff options
| author | Jim Fehrle | 2019-03-27 22:29:22 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2019-03-27 22:29:22 -0700 |
| commit | 21e9d207a8d8a0bee74c000f02a4e2819c53fae5 (patch) | |
| tree | c51cce0fcfbac9676b0a0e66e92dc4e4dce49151 | |
| parent | a796822e5f57f74ff36e538fd2169f70a8c6c145 (diff) | |
| parent | 84f7aa2cdfbe6066c482805336e656b9de6d4762 (diff) | |
Merge PR #9828: Fix syntax of Typeclasses eauto := in reference manual.
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 0a480bdbe7..b069cf27f4 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -575,18 +575,19 @@ Settings Typeclasses eauto `:=` ~~~~~~~~~~~~~~~~~~~~~~ -.. cmd:: Typeclasses eauto := {? debug} {? {dfs | bfs}} depth +.. cmd:: Typeclasses eauto := {? debug} {? (dfs) | (bfs) } @num :name: Typeclasses eauto This command allows more global customization of the typeclass resolution tactic. The semantics of the options are: - + ``debug`` In debug mode, the trace of successfully applied tactics is - printed. This value can also be set with :flag:`Typeclasses Debug`. + + ``debug`` This sets the debug mode. In debug mode, the trace of + successfully applied tactics is printed. The debug mode can also + be set with :flag:`Typeclasses Debug`. - + ``dfs, bfs`` This sets the search strategy to depth-first search (the - default) or breadth-first search. This value can also be set with - :flag:`Typeclasses Iterative Deepening`. + + ``(dfs)``, ``(bfs)`` This sets the search strategy to depth-first + search (the default) or breadth-first search. The search strategy + can also be set with :flag:`Typeclasses Iterative Deepening`. - + ``depth`` This sets the depth limit of the search. This value can also be set with - :opt:`Typeclasses Depth`. + + :token:`num` This sets the depth limit of the search. The depth + limit can also be set with :opt:`Typeclasses Depth`. |