From a90aa1a2d7f0fd12621e744a67cc8c2abd24f9f8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 29 Jun 2018 12:13:00 +0200
Subject: Supporting locality flag for custom entries + compatibility with
 modules.

Also prevents to use an entry name already defined.
---
 test-suite/success/Notations2.v | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v
index d01ebfb18e..1b33863e3b 100644
--- a/test-suite/success/Notations2.v
+++ b/test-suite/success/Notations2.v
@@ -134,3 +134,23 @@ Module M15.
   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.
-- 
cgit v1.2.3