Typeclasses eauto := bfs has no settable max depth

[coqbot]

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#3334
From: @jonleivent
Reported version: trunk
CC: @Zimmi48

[coqbot]

Comment author: @jonleivent

I noticed that, contrary to the reference manual (section 20.6.6), the grammar for the Typeclasses eauto command is more like this:

Typeclasses eauto := [debug] [dfs | depth | bfs].

where depth, if provided, appears to imply dfs as well. This suggests that there is no way to set a maximal depth for bfs. Was this intentional? Certainly, for successful searches, depth matters much more in the depth-first case as a way to prune the search tree.

[coqbot]

Comment author: @Zimmi48

This has been fixed in 8.6 but the documentation needed updating because the syntax had changed. I have created #741 for this.