aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog/07-vernac-commands-and-options/13909-reduce-ambiguous-paths.rst
diff options
context:
space:
mode:
Diffstat (limited to 'doc/changelog/07-vernac-commands-and-options/13909-reduce-ambiguous-paths.rst')
-rw-r--r--doc/changelog/07-vernac-commands-and-options/13909-reduce-ambiguous-paths.rst6
1 files changed, 6 insertions, 0 deletions
diff --git a/doc/changelog/07-vernac-commands-and-options/13909-reduce-ambiguous-paths.rst b/doc/changelog/07-vernac-commands-and-options/13909-reduce-ambiguous-paths.rst
new file mode 100644
index 0000000000..c5a2172005
--- /dev/null
+++ b/doc/changelog/07-vernac-commands-and-options/13909-reduce-ambiguous-paths.rst
@@ -0,0 +1,6 @@
+- **Changed:**
+ Improve the :cmd:`Coercion` command to reduce the number of ambiguous paths to
+ report. A pair of multiple inheritance paths that can be reduced to smaller
+ adjoining pairs will not be reported as ambiguous paths anymore.
+ (`#13909 <https://github.com/coq/coq/pull/13909>`_,
+ by Kazuhiko Sakaguchi).