aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Lists/List.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Lists/List.v')
-rw-r--r--theories/Lists/List.v4
1 files changed, 0 insertions, 4 deletions
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 2cce009a2..f1bcc792d 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -82,10 +82,6 @@ Implicit Arguments nil [A].
Infix "::" := cons (at level 60, right associativity) : list_scope.
Infix "++" := app (right associativity, at level 60) : list_scope.
-Notation "[ ]" := nil : list_scope.
-Notation "[ x ]" := (cons x nil) : list_scope.
-Notation "[ x ; y ; .. ; z ]" := (cons x (cons y .. (cons z nil) .. )) : list_scope.
-
Open Scope list_scope.
Delimit Scope list_scope with list.