aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Lists
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-02-20 13:55:46 +0100
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-03-02 23:45:51 +0100
commita4817d25befc71b7dbf707637660431144985133 (patch)
treefb0d98df0c5678e5a277ff07de82b43bc8a69b7f /theories/Lists
parentff7be36add22cf3c6efd24a27ebdde818fc1dc06 (diff)
Remove VOld compatibility flag.
Diffstat (limited to 'theories/Lists')
-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.