diff options
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/implicit-coercions.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/addendum/ring.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 19 |
3 files changed, 16 insertions, 11 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/ring.rst b/doc/sphinx/addendum/ring.rst index 20e4c6a3d6..3b350d5dc0 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -323,7 +323,7 @@ The syntax for adding a new ring is decidable :n:`@term` declares the ring as computational. The expression :n:`@term` is the correctness proof of an equality test ``?=!`` - (which hould be evaluable). Its type should be of the form + (which should be evaluable). Its type should be of the form ``forall x y, x ?=! y = true → x == y``. morphism :n:`@term` 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`. |