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.v1
1 files changed, 0 insertions, 1 deletions
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index eae2c52de..301528598 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -27,7 +27,6 @@ Module ListNotations.
Notation "[ ]" := nil (format "[ ]") : list_scope.
Notation "[ x ]" := (cons x nil) : list_scope.
Notation "[ x ; y ; .. ; z ]" := (cons x (cons y .. (cons z nil) ..)) : list_scope.
-Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..) (compat "8.4") : list_scope.
End ListNotations.
Import ListNotations.