3 files changed, 17 insertions, 6 deletions
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 6d195b5122..3fd4c1c311 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -194,8 +194,6 @@ pair
             (prod nat (prod nat nat))) (prod (prod nat nat) nat)
 fun x : nat => if x is n .+ 1 then n else 1
      : nat -> nat
-{{{x, y}} : nat * nat | x + y = 0}
-     : Set
 exists2' {{x, y}}, x = 0 & y = 0
      : Prop
 exists2 x : nat * nat,
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index b4ad4a7b3c..9ea218481e 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -341,8 +341,6 @@ Check fun x => if x is n.+1 then n else 1.
 
 (* Examples with binding patterns *)
 
-Check {(x,y)|x+y=0}.
-
 Module D.
 Notation "'exists2'' x , p & q" := (ex2 (fun x => p) (fun x => q))
   (at level 200, x pattern, p at level 200, right associativity,
diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v
index 08d904cea0..7c2cf3ee52 100644
--- a/test-suite/success/Notations2.v
+++ b/test-suite/success/Notations2.v
@@ -98,12 +98,12 @@ Notation "'Funnat' i => t" := (FUNNAT i => t + i%nat) (at level 200).
 
 (* 11. Notations with needed factorization of a recursive pattern *)
 (* See https://github.com/coq/coq/issues/6078#issuecomment-342287412 *)
-Module A.
+Module M11.
 Notation "[:: x1 ; .. ; xn & s ]" := (cons x1 .. (cons xn s) ..).
 Notation "[:: x1 ; .. ; xn ]" := (cons x1 .. (cons xn nil) ..).
 Check [:: 1 ; 2 ; 3 ].
 Check [:: 1 ; 2 ; 3 & nil ]. (* was failing *)
-End A.
+End M11.
 
 (* 12. Preventively check that a variable which does not occur can be instantiated *)
 (* by any term. In particular, it should not be restricted to a binder *)
@@ -111,3 +111,18 @@ Module M12.
 Notation "N ++ x" := (S x) (only parsing).
 Check 2 ++ 0.
 End M12.
+
+(* 13. Check that internal data about associativity are not used in comparing levels *)
+Module M13.
+Notation "x ;; z" := (x + z)
+  (at level 100, z at level 200, only parsing, right associativity).
+Notation "x ;; z" := (x * z)
+  (at level 100, z at level 200, only parsing) : foo_scope.
+End M13.
+
+(* 14. Check that a notation with a "ident" binder does not include a pattern *)
+Module M14.
+Notation "'myexists' x , p" := (ex (fun x => p))
+  (at level 200, x ident, p at level 200, right associativity) : type_scope.
+Check myexists I, I = 0. (* Should not be seen as a constructor *)
+End M14.