diff options
| author | Théo Zimmermann | 2019-03-25 16:44:54 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-03-26 10:02:01 +0100 |
| commit | 84f7aa2cdfbe6066c482805336e656b9de6d4762 (patch) | |
| tree | dcf331a12241154823a65ef9d684ca53a2cd92bb /doc | |
| parent | fd065eae52dde32bcb95955f6da9280fed780729 (diff) | |
Fix syntax of Typeclasses eauto := in reference manual.
Diffstat (limited to 'doc')
| -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 e6a5b3972c..3f5035d4a4 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -573,18 +573,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`. |