diff options
| author | Kazuhiko Sakaguchi | 2019-06-06 16:05:52 +0200 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2019-06-06 16:19:08 +0200 |
| commit | 8c53c2909511a6ff324ac39bb0ff1040c04de712 (patch) | |
| tree | 5b1e0907869dc7ea6fd872bea4e7fe388bbfc7f7 | |
| parent | 4f7af2b09a935528d660a354f5e7672fc92e9a5c (diff) | |
Update changes.rst as a follow-up to #9743
| -rw-r--r-- | doc/sphinx/changes.rst | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index db4ebd5e38..bfc7e072b7 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -525,7 +525,13 @@ Other changes in 8.10+beta1 (`#9829 <https://github.com/coq/coq/pull/9829>`_, by Vincent Laporte). - :cmd:`Coercion` does not warn ambiguous paths which are obviously - convertible with existing ones + convertible with existing ones. The ambiguous paths messages have been + turned to warnings, thus now they could appear in the output of ``coqc``. + The convertibility checking procedure for coercion paths is complete for + paths consisting of coercions satisfying the uniform inheritance condition, + but some coercion paths could be reported as ambiguous even if they are + convertible with existing ones when they have coercions that don't satisfy + the uniform inheritance condition (`#9743 <https://github.com/coq/coq/pull/9743>`_, closes `#3219 <https://github.com/coq/coq/issues/3219>`_, by Kazuhiko Sakaguchi). |