Unbreak singleton list-like notation (-compat 8.4)

With this commit, it is possible to write notations so that singleton
lists are usable in both 8.4 and 8.5pl1 -compat.  Longer lists await the
ability to remove notations from the parser.

3 files changed, 118 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/4684.v b/test-suite/bugs/closed/4684.v
new file mode 100644
index 000000000..9c0bed42c
--- /dev/null
+++ b/test-suite/bugs/closed/4684.v
@@ -0,0 +1,32 @@
+(*Suppose a user wants to declare a new list-like notation with support for singletons in both 8.4 and 8.5.  If they use*)
+Require Import Coq.Lists.List.
+Require Import Coq.Vectors.Vector.
+Import ListNotations.
+Import VectorNotations.
+Set Implicit Arguments.
+Inductive mylist T := mynil | mycons (_ : T) (_ : mylist T).
+Arguments mynil {_}, _.
+
+Delimit Scope mylist_scope with mylist.
+Bind Scope mylist_scope with mylist.
+Delimit Scope vector_scope with vector.
+
+Notation " [ ] " := mynil (format "[ ]") : mylist_scope.
+Notation " [ x ] " := (mycons x mynil) : mylist_scope.
+Notation " [ x ; y ; .. ; z ] " := (mycons x (mycons y .. (mycons z mynil) ..)) : mylist_scope.
+
+Check [ ]%mylist : mylist _.
+Check [ ]%list : list _.
+Check []%vector : Vector.t _ _.
+Check [ _ ]%mylist : mylist _.
+Check [ _ ]%list : list _.
+Check [ _ ]%vector : Vector.t _ _.
+Check [ _ ; _ ]%list : list _.
+Check [ _ ; _ ]%vector : Vector.t _ _.
+Check [ _ ; _ ]%mylist : mylist _.
+Check [ _ ; _ ; _ ]%list : list _.
+Check [ _ ; _ ; _ ]%vector : Vector.t _ _.
+Check [ _ ; _ ; _ ]%mylist : mylist _.
+Check [ _ ; _ ; _ ; _ ]%list : list _.
+Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _.
+Check [ _ ; _ ; _ ; _ ]%mylist : mylist _.
diff --git a/test-suite/bugs/closed/4733.v b/test-suite/bugs/closed/4733.v
new file mode 100644
index 000000000..ac0653492
--- /dev/null
+++ b/test-suite/bugs/closed/4733.v
@@ -0,0 +1,52 @@
+(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *)
+(*Suppose a user wants to declare a new list-like notation with support for singletons in both 8.4 and 8.5.  If they use*)
+Require Import Coq.Lists.List.
+Require Import Coq.Vectors.Vector.
+Import ListNotations.
+Import VectorNotations.
+Set Implicit Arguments.
+Inductive mylist T := mynil | mycons (_ : T) (_ : mylist T).
+Arguments mynil {_}, _.
+
+Delimit Scope mylist_scope with mylist.
+Bind Scope mylist_scope with mylist.
+Delimit Scope vector_scope with vector.
+
+Notation " [ ] " := mynil (format "[ ]") : mylist_scope.
+Notation " [ x ] " := (mycons x mynil) : mylist_scope.
+Notation " [ x ; .. ; y ] " := (mycons x .. (mycons y mynil) ..) : mylist_scope.
+
+(** All of these should work fine in -compat 8.4 mode, just as they do in Coq 8.4.  There needs to be a way to specify notations above so that all of these [Check]s go through in both 8.4 and 8.5 *)
+Check [ ]%mylist : mylist _.
+Check [ ]%list : list _.
+Check []%vector : Vector.t _ _.
+Check [ _ ]%mylist : mylist _.
+Check [ _ ]%list : list _.
+Check [ _ ]%vector : Vector.t _ _.
+Check [ _ ; _ ]%list : list _.
+Check [ _ ; _ ]%vector : Vector.t _ _.
+Fail Check [ _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *)
+Check [ _ ; _ ; _ ]%list : list _.
+Check [ _ ; _ ; _ ]%vector : Vector.t _ _.
+Fail Check [ _ ; _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *)
+Check [ _ ; _ ; _ ; _ ]%list : list _.
+Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _.
+Fail Check [ _ ; _ ; _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *)
+
+Notation " [ x ; y ; .. ; z ] " := (mycons x (mycons y .. (mycons z mynil) ..)) : mylist_scope.
+(* Now these all work, but not so in 8.4.  If we get the ability to remove notations, and the above fails can be removed, this section can also just be removed. *)
+Check [ ]%mylist : mylist _.
+Check [ ]%list : list _.
+Check []%vector : Vector.t _ _.
+Check [ _ ]%mylist : mylist _.
+Check [ _ ]%list : list _.
+Check [ _ ]%vector : Vector.t _ _.
+Check [ _ ; _ ]%list : list _.
+Check [ _ ; _ ]%vector : Vector.t _ _.
+Check [ _ ; _ ]%mylist : mylist _.
+Check [ _ ; _ ; _ ]%list : list _.
+Check [ _ ; _ ; _ ]%vector : Vector.t _ _.
+Check [ _ ; _ ; _ ]%mylist : mylist _.
+Check [ _ ; _ ; _ ; _ ]%list : list _.
+Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _.
+Check [ _ ; _ ; _ ; _ ]%mylist : mylist _.
diff --git a/test-suite/bugs/opened/4803.v b/test-suite/bugs/opened/4803.v
new file mode 100644
index 000000000..3ca5c095f
--- /dev/null
+++ b/test-suite/bugs/opened/4803.v
@@ -0,0 +1,34 @@
+(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *)
+(*Suppose a user wants to declare a new list-like notation with support for singletons in both 8.4 and 8.5.  If they use*)
+Require Import Coq.Lists.List.
+Require Import Coq.Vectors.Vector.
+Import ListNotations.
+Import VectorNotations.
+Set Implicit Arguments.
+Inductive mylist T := mynil | mycons (_ : T) (_ : mylist T).
+Arguments mynil {_}, _.
+
+Delimit Scope mylist_scope with mylist.
+Bind Scope mylist_scope with mylist.
+Delimit Scope vector_scope with vector.
+
+Notation " [ ] " := mynil (format "[ ]") : mylist_scope.
+Notation " [ x ] " := (mycons x mynil) : mylist_scope.
+Notation " [ x ; .. ; y ] " := (mycons x .. (mycons y mynil) ..) : mylist_scope.
+
+(** All of these should work fine in -compat 8.4 mode, just as they do in Coq 8.4.  There needs to be a way to specify notations above so that all of these [Check]s go through in both 8.4 and 8.5 *)
+Check [ ]%mylist : mylist _.
+Check [ ]%list : list _.
+Check []%vector : Vector.t _ _.
+Check [ _ ]%mylist : mylist _.
+Check [ _ ]%list : list _.
+Check [ _ ]%vector : Vector.t _ _.
+Check [ _ ; _ ]%list : list _.
+Check [ _ ; _ ]%vector : Vector.t _ _.
+Fail Check [ _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser; it should be added to Compat/Coq84.v *)
+Check [ _ ; _ ; _ ]%list : list _.
+Check [ _ ; _ ; _ ]%vector : Vector.t _ _.
+Fail Check [ _ ; _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *)
+Check [ _ ; _ ; _ ; _ ]%list : list _.
+Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _.
+Fail Check [ _ ; _ ; _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *)