diff options
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/implicit-coercions.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 19 |
2 files changed, 15 insertions, 10 deletions
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index 795fccbf08..d5523e8561 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -154,8 +154,10 @@ Declaring Coercions .. warn:: Ambiguous path. When the coercion :token:`qualid` is added to the inheritance graph, - invalid coercion paths are ignored; they are signaled by a warning - displaying these paths of the form :g:`[f₁;..;fₙ] : C >-> D`. + invalid coercion paths are ignored. The :cmd:`Coercion` command tries to check + that they are convertible with existing ones on the same classes. + The paths for which this check fails are displayed by a warning in the form + :g:`[f₁;..;fₙ] : C >-> D`. .. cmdv:: Local Coercion @qualid : @class >-> @class diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index e6a5b3972c..b069cf27f4 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -561,6 +561,8 @@ Settings .. flag:: Refine Instance Mode + .. deprecated:: 8.10 + This flag allows to switch the behavior of instance declarations made through the Instance command. @@ -573,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`. |