diff options
| author | Théo Zimmermann | 2019-06-14 17:59:09 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-06-14 17:59:09 +0200 |
| commit | a024cf9c61b57860ce3e679be4fae427996320db (patch) | |
| tree | 3bfedcb2eef51882e6dea690ca67796850f5e795 | |
| parent | f0d0fedd7e8ac8fbbe9f6128ea17b97792cd4dfc (diff) | |
| parent | 8c53c2909511a6ff324ac39bb0ff1040c04de712 (diff) | |
Merge PR #10322: Update changes.rst as a follow-up to #9743
Reviewed-by: Zimmi48
| -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 84e8da2292..6ff15e52a3 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -527,7 +527,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). |