From 84f7aa2cdfbe6066c482805336e656b9de6d4762 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 25 Mar 2019 16:44:54 +0100
Subject: Fix syntax of Typeclasses eauto := in reference manual.

---
 doc/sphinx/addendum/type-classes.rst | 17 +++++++++--------
 1 file 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`.
-- 
cgit v1.2.3