From 8a57a4aa808c10f554020e47d5e4173b14bd471d Mon Sep 17 00:00:00 2001
From: Yishuai Li
Date: Wed, 25 Jul 2018 12:27:17 -0400
Subject: Vector: expose ++ to user

---
 CHANGES                      | 4 ++++
 theories/Vectors/VectorDef.v | 1 +
 2 files changed, 5 insertions(+)

diff --git a/CHANGES b/CHANGES
index aaf079602f..c1c54ee4b9 100644
--- a/CHANGES
+++ b/CHANGES
@@ -139,6 +139,10 @@ Display diffs between proof steps
   details.  Showing diffs in Proof General requires small changes to PG
   (under discussion).
 
+Notations
+
+- Added [++] infix for [VectorDef.append].
+
 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.
-- 
cgit v1.2.3