aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Lists
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Lists')
-rw-r--r--theories/Lists/List.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index cc7586fec..957f1066d 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -26,7 +26,7 @@ In a special module to avoid conflicts. *)
Module ListNotations.
Notation " [ ] " := nil (format "[ ]") : list_scope.
Notation " [ x ] " := (cons x nil) : list_scope.
-Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope.
+Notation " [ x ; y ; .. ; z ] " := (cons x (cons y .. (cons z nil) ..)) : list_scope.
End ListNotations.
Import ListNotations.