From 7bc04ff2cc9d511c4b8552a3e5f9ad416917fb95 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Sat, 11 Jun 2016 17:23:08 -0400
Subject: 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.
---
 test-suite/bugs/closed/4785.v | 26 ++++++++++++++++++++++++++
 1 file changed, 26 insertions(+)
 create mode 100644 test-suite/bugs/closed/4785.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4785.v b/test-suite/bugs/closed/4785.v
new file mode 100644
index 0000000000..b844af68a9
--- /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 _.
-- 
cgit v1.2.3