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.

1 files changed, 17 insertions, 3 deletions

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 { _ : _ & _ }. *)