From cc6526b17ca6ee8cd48e83428282421a004c1763 Mon Sep 17 00:00:00 2001
From: Yishuai Li
Date: Fri, 27 Jul 2018 16:34:15 -0400
Subject: CHANGES: note potential incompatibilities with ++

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

diff --git a/CHANGES b/CHANGES
index c1c54ee4b9..b0b445b2e8 100644
--- a/CHANGES
+++ b/CHANGES
@@ -142,6 +142,10 @@ Display diffs between proof steps
 Notations
 
 - Added [++] infix for [VectorDef.append].
+  Note that this might cause incompatibilities if you have, e.g., list_scope
+  and vector_scope both open with vector_scope on top, and expect `++` to
+  refer to `app`.
+  Solution: wrap `_ ++ _` in `(_ ++ _)%list` (or whichever scope you want). 
 
 Changes from 8.8.0 to 8.8.1
 ===========================
-- 
cgit v1.2.3