A word about PR #262 in CHANGES.

1 files changed, 6 insertions, 1 deletions

diff --git a/CHANGES b/CHANGES
index b2f2987249..e16da2ab2d 100644
--- a/CHANGES
+++ b/CHANGES
@@ -83,7 +83,7 @@ Focusing
   e.g. `[x]: {` will focus on a goal (existential variable) named `x`.
   As usual, unfocus with `}` once the sub-goal is fully solved.
 
-Specification language
+Specification language, type inference
 
 - A fix to unification (which was sensitive to the ascii name of
   variables) may occasionally change type inference in incompatible
@@ -94,6 +94,11 @@ Specification language
   induce an overhead if the cost of checking the conversion of the
   corresponding definitions is additionally high (PR #8215).
 
+- A few improvements in inference of the return clause of "match" can
+  exceptionally introduce incompatibilities (PR #262). This can be
+  solved by writing an explicit "return" clause, sometimes even simply
+  an explicit "return _" clause.
+
 Standard Library
 
 - Added `Ascii.eqb` and `String.eqb` and the `=?` notation for them,