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

2 files changed, 9 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
 ===========================
 
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index f6f3cafa21..ba3e411091 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -312,5 +312,6 @@ Notation "h :: t" := (h :: t) (at level 60, right associativity)
 Notation "[ x ]" := (x :: []) : vector_scope.
 Notation "[ x ; y ; .. ; z ]" := (cons _ x _ (cons _ y _ .. (cons _ z _ (nil _)) ..)) : vector_scope.
 Notation "v [@ p ]" := (nth v p) (at level 1, format "v [@ p ]") : vector_scope.
+Infix "++" := append : vector_scope.
 Open Scope vector_scope.
 End VectorNotations.