Fix bug #4785 (use [ ] for vector nil)

Also delimit vector_scope with vector, so that people can write %vector
without having to delimit it themselves.

1 files changed, 26 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/4785.v b/test-suite/bugs/closed/4785.v
new file mode 100644
index 000000000..b844af68a
--- /dev/null
+++ b/test-suite/bugs/closed/4785.v
@@ -0,0 +1,26 @@
+Require Import Coq.Lists.List Coq.Vectors.Vector.
+Import ListNotations.
+Check [ ]%list : list _.
+Import VectorNotations ListNotations.
+Delimit Scope vector_scope with vector.
+Check [ ]%vector : Vector.t _ _.
+Check []%vector : Vector.t _ _.
+Check [ ]%list : list _.
+Check []%list : list _.
+
+Inductive mylist A := mynil | mycons (x : A) (xs : mylist A).
+Delimit Scope mylist_scope with mylist.
+Bind Scope mylist_scope with mylist.
+Arguments mynil {_}, _.
+Arguments mycons {_} _ _.
+Notation " [] " := mynil : mylist_scope.
+Notation " [ ] " := mynil (format "[ ]") : mylist_scope.
+Notation " [ x ] " := (mycons x nil) : mylist_scope.
+Notation " [ x ; y ; .. ; z ] " :=  (mycons x (mycons y .. (mycons z nil) ..)) : mylist_scope.
+
+Require Import Coq.Compat.Coq85.
+
+Check []%vector : Vector.t _ _.
+Check []%mylist : mylist _.
+Check [ ]%mylist : mylist _.
+Check [ ]%list : list _.