diff options
| author | Kazuhiko Sakaguchi | 2019-03-18 14:12:23 +0100 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2019-03-18 14:12:23 +0100 |
| commit | 7637dc2dd51dd336249cefa828ec95790b3c88c5 (patch) | |
| tree | b2a2ba725761cf05115b6aefce95d6cc3568c1bd | |
| parent | 5c388bb330afab9b87ab68ee94e4dc1055bf66f9 (diff) | |
Update doc and changes
| -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 |