diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/07-commands-and-options/11258-coherence.rst | 10 | ||||
| -rw-r--r-- | doc/sphinx/addendum/implicit-coercions.rst | 6 |
2 files changed, 16 insertions, 0 deletions
diff --git a/doc/changelog/07-commands-and-options/11258-coherence.rst b/doc/changelog/07-commands-and-options/11258-coherence.rst new file mode 100644 index 0000000000..f04a120417 --- /dev/null +++ b/doc/changelog/07-commands-and-options/11258-coherence.rst @@ -0,0 +1,10 @@ +- **Changed:** + The :cmd:`Coercion` command has been improved to check the coherence of the + inheritance graph. It checks whether a circular inheritance path of `C >-> C` + is convertible with the identity function or not, then report it as an + ambiguous path if it is not. The new mechanism does not report ambiguous + paths that are redundant with others. For example, checking the ambiguity of + `[f; g]` and `[f'; g]` is redundant with that of `[f]` and `[f']` thus will + not be reported + (`#11258 <https://github.com/coq/coq/pull/11258>`_, + by Kazuhiko Sakaguchi). diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index c3b197288f..19b33f0d90 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -165,6 +165,12 @@ Declaring Coercions convertible with existing ones when they have coercions that don't satisfy the uniform inheritance condition. + .. warn:: ... is not definitionally an identity function. + + If a coercion path has the same source and target class, that is said to be + circular. When a new circular coercion path is not convertible with the + identity function, it will be reported as ambiguous. + .. cmdv:: Local Coercion @qualid : @class >-> @class Declares the construction denoted by :token:`qualid` as a coercion local to |