Merge PR #8151: Vector: expose ++ to user

1 files changed, 8 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index aaf079602f..f0327e74dc 100644
--- a/CHANGES
+++ b/CHANGES
@@ -139,6 +139,14 @@ Display diffs between proof steps
   details.  Showing diffs in Proof General requires small changes to PG
   (under discussion).
 
+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
 ===========================