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.

9 files changed, 78 insertions, 35 deletions

diff --git a/test-suite/bugs/closed/4733.v b/test-suite/bugs/closed/4733.v
index ac0653492..a6ebda61c 100644
--- a/test-suite/bugs/closed/4733.v
+++ b/test-suite/bugs/closed/4733.v
@@ -25,16 +25,16 @@ 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 [ _ ; _ ]%mylist : mylist _.
 Check [ _ ; _ ; _ ]%list : list _.
 Check [ _ ; _ ; _ ]%vector : Vector.t _ _.
-Fail Check [ _ ; _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *)
+Check [ _ ; _ ; _ ]%mylist : mylist _.
 Check [ _ ; _ ; _ ; _ ]%list : list _.
 Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _.
-Fail Check [ _ ; _ ; _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *)
+Check [ _ ; _ ; _ ; _ ]%mylist : mylist _.
 
 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. *)
+(* Now these all work, but not so in 8.4.  If we get the ability to remove notations, this section can also just be removed. *)
 Check [ ]%mylist : mylist _.
 Check [ ]%list : list _.
 Check []%vector : Vector.t _ _.
diff --git a/test-suite/bugs/closed/4785.v b/test-suite/bugs/closed/4785.v
index 14af2d91d..c3c97d3f5 100644
--- a/test-suite/bugs/closed/4785.v
+++ b/test-suite/bugs/closed/4785.v
@@ -21,7 +21,7 @@ Delimit Scope mylist_scope with mylist.
 Bind Scope mylist_scope with mylist.
 Arguments mynil {_}, _.
 Arguments mycons {_} _ _.
-Notation " [] " := mynil : mylist_scope.
+Notation " [] " := mynil (compat "8.5") : 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.
diff --git a/test-suite/bugs/closed/4785_compat_85.v b/test-suite/bugs/closed/4785_compat_85.v
new file mode 100644
index 000000000..9d65840ac
--- /dev/null
+++ b/test-suite/bugs/closed/4785_compat_85.v
@@ -0,0 +1,46 @@
+(* -*- coq-prog-args: ("-emacs" "-compat" "8.5") -*- *)
+Require Coq.Lists.List Coq.Vectors.Vector.
+Require Coq.Compat.Coq85.
+
+Module A.
+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 _.
+Fail Check []%list : list _.
+
+Goal True.
+  idtac; [ ]. (* Note that vector notations break the [ | .. | ] syntax of Ltac *)
+Abort.
+
+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 (compat "8.5") : 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.
+
+Import Coq.Compat.Coq85.
+Locate Module VectorNotations.
+Import VectorDef.VectorNotations.
+
+Check []%vector : Vector.t _ _.
+Check []%mylist : mylist _.
+Check [ ]%mylist : mylist _.
+Check [ ]%list : list _.
+End A.
+
+Module B.
+Import Coq.Compat.Coq85.
+
+Goal True.
+  idtac; []. (* Check that importing the compat file doesn't break the [ | .. | ] syntax of Ltac *)
+Abort.
+End B.
diff --git a/test-suite/bugs/opened/4803.v b/test-suite/bugs/opened/4803.v
index 3ca5c095f..4530548b8 100644
--- a/test-suite/bugs/opened/4803.v
+++ b/test-suite/bugs/opened/4803.v
@@ -25,10 +25,24 @@ 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 [ _ ; _ ]%mylist : mylist _.
 Check [ _ ; _ ; _ ]%list : list _.
 Check [ _ ; _ ; _ ]%vector : Vector.t _ _.
-Fail Check [ _ ; _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *)
+Check [ _ ; _ ; _ ]%mylist : mylist _.
 Check [ _ ; _ ; _ ; _ ]%list : list _.
 Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _.
-Fail Check [ _ ; _ ; _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *)
+Check [ _ ; _ ; _ ; _ ]%mylist : mylist _.
+
+(** Now check that we can add and then remove notations from the parser *)
+(* We should be able to stick some vernacular here to remove [] from the parser *)
+Fail Remove Notation "[]".
+Goal True.
+  (* This should not be a syntax error; before moving this file to closed, uncomment this line. *)
+  (* idtac; []. *)
+  constructor.
+Qed.
+
+Check { _ : _ & _ }.
+Reserved Infix "&" (at level 0).
+Fail Remove Infix "&".
+(* Check { _ : _ & _ }. *)
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 2f7c62972..30abd961b 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -58,7 +58,7 @@ Check (fun x:nat*nat => match x with R x y => (x,y) end).
 
 (* Check multi-tokens recursive notations *)
 
-Local Notation "[ a  # ; ..  # ; b ]" := (a + .. (b + 0) ..).   
+Local Notation "[ a  # ; ..  # ; b ]" := (a + .. (b + 0) ..).
 Check [ 0 ].
 Check [ 0 # ; 1 ].
 
@@ -110,3 +110,8 @@ Goal True -> True. intros H. exact H. Qed.
 
 (* Check absence of collision on ".." in nested notations with ".." *)
 Notation "[ a , .. , b ]" := (a, (.. (b,tt) ..)).
+
+(* Check that vector notations do not break Ltac [] (bugs #4785, #4733) *)
+Require Import Coq.Vectors.VectorDef.
+Import VectorNotations.
+Goal True. idtac; []. (* important for test: no space here *) constructor. Qed.
diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v
index 5eecdc64c..a3e23f91c 100644
--- a/theories/Compat/Coq84.v
+++ b/theories/Compat/Coq84.v
@@ -74,12 +74,6 @@ Coercion sig_of_sigT : sigT >-> sig.
 Coercion sigT2_of_sig2 : sig2 >-> sigT2.
 Coercion sig2_of_sigT2 : sigT2 >-> sig2.
 
-(** As per bug #4733 (https://coq.inria.fr/bugs/show_bug.cgi?id=4733), we want the user to be able to create custom list-like notatoins that work in both 8.4 and 8.5.  This is necessary.  These should become compat 8.4 notations in the relevant files, but these modify the parser (bug #4798), so this cannot happen until that bug is fixed. *)
-Require Coq.Lists.List.
-Require Coq.Vectors.VectorDef.
-Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..) : list_scope.
-Notation "[ x ; .. ; y ]" := (VectorDef.cons _ x _ .. (VectorDef.cons _ y _ (nil _)) ..) : vector_scope.
-
 (** In 8.4, the statement of admitted lemmas did not depend on the section
     variables. *)
 Unset Keep Admitted Variables.
diff --git a/theories/Compat/Coq85.v b/theories/Compat/Coq85.v
index 54aeeaa11..490e95c91 100644
--- a/theories/Compat/Coq85.v
+++ b/theories/Compat/Coq85.v
@@ -22,21 +22,3 @@ Global Unset Structural Injection.
 Global Unset Shrink Abstract.
 Global Unset Shrink Obligations.
 Global Set Refolding Reduction.
-
-(** In Coq 8.5, [] meant Vector, and [ ] meant list.  Restore this
-    behavior, to allow user-defined [] to not override vector
-    notations.  See https://coq.inria.fr/bugs/show_bug.cgi?id=4785. *)
-
-Require Coq.Lists.List.
-Require Coq.Vectors.VectorDef.
-Module Export Coq.
-Module Export Vectors.
-Module VectorDef.
-Export Coq.Vectors.VectorDef.
-Module VectorNotations.
-Export Coq.Vectors.VectorDef.VectorNotations.
-Notation "[]" := (VectorDef.nil _) : vector_scope.
-End VectorNotations.
-End VectorDef.
-End Vectors.
-End Coq.
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.
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index f49b34075..1f8b76cb6 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -295,11 +295,12 @@ End VECTORLIST.
 Module VectorNotations.
 Delimit Scope vector_scope with vector.
 Notation "[ ]" := [] (format "[ ]") : vector_scope.
+Notation "[]" := [] (compat "8.5") : vector_scope.
 Notation "h :: t" := (h :: t) (at level 60, right associativity)
   : vector_scope.
 Notation "[ x ]" := (x :: []) : vector_scope.
-Notation "[ x ; y ; .. ; z ]" := (cons _ x _ (cons _ y _ .. (cons _ z _ (nil _)) ..)) : vector_scope
-.
+Notation "[ x ; y ; .. ; z ]" := (cons _ x _ (cons _ y _ .. (cons _ z _ (nil _)) ..)) : vector_scope.
+Notation "[ x ; .. ; y ]" := (cons _ x _ .. (cons _ y _ (nil _)) ..) (compat "8.4") : vector_scope.
 Notation "v [@ p ]" := (nth v p) (at level 1, format "v [@ p ]") : vector_scope.
 Open Scope vector_scope.
 End VectorNotations.