From 48bded44b715a1ebb351ee0cb1ce1bac63a4ce4f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 15 Mar 2019 11:11:43 +0100
Subject: [PATCH] Put list notations like `(++)` in `list_scope` instead of
 `stdpp_scope`.

---
 theories/list.v | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/theories/list.v b/theories/list.v
index 0bd8b49d..a1884005 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -30,12 +30,12 @@ Arguments Permutation {_} _ _ : assert.
 Arguments Forall_cons {_} _ _ _ _ _ : assert.
 Remove Hints Permutation_cons : typeclass_instances.
 
-Notation "(::)" := cons (only parsing) : stdpp_scope.
-Notation "( x ::)" := (cons x) (only parsing) : stdpp_scope.
-Notation "(:: l )" := (λ x, cons x l) (only parsing) : stdpp_scope.
-Notation "(++)" := app (only parsing) : stdpp_scope.
-Notation "( l ++)" := (app l) (only parsing) : stdpp_scope.
-Notation "(++ k )" := (λ l, app l k) (only parsing) : stdpp_scope.
+Notation "(::)" := cons (only parsing) : list_scope.
+Notation "( x ::)" := (cons x) (only parsing) : list_scope.
+Notation "(:: l )" := (λ x, cons x l) (only parsing) : list_scope.
+Notation "(++)" := app (only parsing) : list_scope.
+Notation "( l ++)" := (app l) (only parsing) : list_scope.
+Notation "(++ k )" := (λ l, app l k) (only parsing) : list_scope.
 
 Infix "≡ₚ" := Permutation (at level 70, no associativity) : stdpp_scope.
 Notation "(≡ₚ)" := Permutation (only parsing) : stdpp_scope.
-- 
GitLab