From fcd903c299db00d5c8d3e2fa797404eb880b61ac Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 19 Dec 2019 18:03:34 +0100
Subject: Ensure that a custom entry cannot be defined twice.

This highlights the fact that diamond inheritance of a custom entry
is a tricky problem, as well as merely importing two custom entries with
the same name from two different modules. The only sane way to give a
semantics to that is to stick to module-scoped objects, i.e. give those
entries a kernel name. In the meantime, I went for a warning when
overriding entries.
---
 test-suite/success/custom_entry.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create mode 100644 test-suite/success/custom_entry.v

(limited to 'test-suite')

diff --git a/test-suite/success/custom_entry.v b/test-suite/success/custom_entry.v
new file mode 100644
index 0000000000..e88ae65e18
--- /dev/null
+++ b/test-suite/success/custom_entry.v
@@ -0,0 +1,13 @@
+Declare Custom Entry foo.
+
+Print Custom Grammar foo.
+
+Notation "[ e ]" := e (e custom foo at level 0).
+
+Print Custom Grammar foo.
+
+Notation "1" := O (in custom foo at level 0).
+
+Print Custom Grammar foo.
+
+Fail Declare Custom Entry foo.
-- 
cgit v1.2.3