diff --git a/theories/list.v b/theories/list.v
index 0bd8b49da77e1bf28e9502eab336a4f46d3f1f7c..a18840055138606e5de8ea58a827ba5a9c69253d 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.