Merge PR #8115: Support for custom entries in notations (take 2, feature part)

1 files changed, 28 insertions, 0 deletions

diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v
index 7c2cf3ee52..1b33863e3b 100644
--- a/test-suite/success/Notations2.v
+++ b/test-suite/success/Notations2.v
@@ -126,3 +126,31 @@ 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.
+
+(* 15. Testing different ways to give the same levels without failing *)
+
+Module M15.
+  Local Notation "###### x" := (S x) (right associativity, at level 79, x at next level).
+  Fail Local Notation "###### x" := (S x) (right associativity, at level 79).
+  Local Notation "###### x" := (S x) (at level 79).
+End M15.
+
+(* 16. Some test about custom entries *)
+Module M16.
+  (* Test locality *)
+  Local Declare Custom Entry foo.
+  Fail Notation "#" := 0 (in custom foo). (* Should be local *)
+  Local Notation "#" := 0 (in custom foo).
+
+  (* Test import *)
+  Module A.
+  Declare Custom Entry foo2.
+  End A.
+  Fail Notation "##" := 0 (in custom foo2).
+  Import A.
+  Local Notation "##" := 0 (in custom foo2).
+
+  (* Test Print Grammar *)
+  Print Grammar foo.
+  Print Grammar foo2.
+End M16.