From f20a053364421c6f5691bb02c9015a9db5cbfafe Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 10 May 2018 15:23:45 +0200
Subject: Notations: advertize that distinct "only parsing"/"only printing"
 rules work.

---
 CHANGES | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/CHANGES b/CHANGES
index 68cc495f58..cdc1ff6a63 100644
--- a/CHANGES
+++ b/CHANGES
@@ -33,6 +33,14 @@ Tactic language
   called by OCaml-defined tactics.
 - Option "Ltac Debug" now applies also to terms built using Ltac functions.
 
+Changes from 8.8.0 to 8.8.1
+===========================
+
+Notations
+
+- Fixed unexpected collision between only-parsing and only-printing
+  notations (issue #7462).
+
 Changes from 8.8+beta1 to 8.8.0
 ===============================
 
-- 
cgit v1.2.3