CHANGES: note potential incompatibilities with ++

1 files changed, 4 insertions, 0 deletions

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
 ===========================