diff options
| -rw-r--r-- | CHANGES.md | 3 | ||||
| -rw-r--r-- | doc/sphinx/addendum/implicit-coercions.rst | 6 |
2 files changed, 7 insertions, 2 deletions
diff --git a/CHANGES.md b/CHANGES.md index 59cc17c233..cf32300ce9 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -140,6 +140,9 @@ Vernacular commands - `Hypotheses` and `Variables` can now take implicit binders inside sections. +- `Coercion` does not warn ambiguous paths which are obviously convertible with + existing ones. + Tools - The `-native-compiler` flag of `coqc` and `coqtop` now takes an argument which can have three values: diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index d15aacad44..58bd96951b 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 |