From bfbc82eb29c9dbf868d3decbd30b0462ea398ebd Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 25 May 2018 18:33:26 +0200
Subject: A word about PR #262 in CHANGES.

---
 CHANGES | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

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,
-- 
cgit v1.2.3