Fix #11121: Simultaneous definition of term and notation in custom grammar

1 files changed, 21 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/bug_11121.v b/test-suite/bugs/closed/bug_11121.v
new file mode 100644
index 0000000000..6112a443ab
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11121.v
@@ -0,0 +1,21 @@
+Declare Custom Entry example.
+
+Module M1.
+Fixpoint stupid (x : nat) : nat := 1.
+Reserved Notation " x '==' 1 " (in custom example at level 0, x constr).
+Notation " x '==' 1" := (stupid x) (in custom example).
+End M1.
+
+Module M2.
+Fixpoint stupid (x : nat) : nat := 1.
+Notation " x '==' 1" := (stupid x) (in custom example at level 0).
+Fail Notation " x '==' 1" := (stupid x) (in custom example at level 1).
+End M2.
+
+Module M3.
+Reserved Notation " x '==' 1 " (in custom example at level 55, x constr).
+
+Fixpoint stupid (x : nat) : nat := 1
+where " x '==' 1" := (stupid x) (in custom example).
+
+End M3.