Merge PR #300 into v8.6

8 files changed, 78 insertions, 17 deletions

diff --git a/test-suite/bugs/closed/4733.v b/test-suite/bugs/closed/4733.v
index ac0653492a..a6ebda61cf 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 14af2d91df..c3c97d3f59 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 0000000000..9d65840acd
--- /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 3ca5c095f5..4530548b8f 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 2f7c62972a..30abd961b1 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 5eecdc64cc..a3e23f91c9 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/Lists/List.v b/theories/Lists/List.v
index fc94d7e254..bf21ffb47b 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 f49b340758..1f8b76cb62 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.