1 files changed, 1 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 41c2138ef3..974a16a938 100644
--- a/CHANGES
+++ b/CHANGES
@@ -5,6 +5,7 @@ Language
 
 - Slightly improved compilation of pattern-matching (slight source of
   incompatibilities)
+- Record's now accept anonymous fields "_" which does not build projections
 
 Tactics