From 1a3fc19d1160cb3896e62a16c8e68c97880c748b Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 29 Sep 2016 14:00:34 -0400 Subject: Move vector/list compat notations to their relevant files Since edb55a94fc5c0473e57f5a61c0c723194c2ff414 landed, compat notations no longer modify the parser in non-compat-mode, so we can do this without breaking Ltac parsing. Also update the related test-suite files. --- theories/Lists/List.v | 1 + 1 file changed, 1 insertion(+) (limited to 'theories/Lists') diff --git a/theories/Lists/List.v b/theories/Lists/List.v index fc94d7e25..bf21ffb47 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -27,6 +27,7 @@ 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. -- cgit v1.2.3