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


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


From 8c14ee1bc5e3daf2c836badf1aadef3ecb87c99c Mon Sep 17 00:00:00 2001
From: Yishuai Li
Date: Mon, 30 Jul 2018 13:32:07 -0400
Subject: CHANGES: unify format

---
 CHANGES | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/CHANGES b/CHANGES
index b0b445b2e8..f0327e74dc 100644
--- a/CHANGES
+++ b/CHANGES
@@ -141,7 +141,7 @@ Display diffs between proof steps
 
 Notations
 
-- Added [++] infix for [VectorDef.append].
+- 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`.
-- 
cgit v1.2.3