From 53e19f76624b7a18792af799e970e9478f8e90a9 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 16 Jun 2020 17:09:40 +0200
Subject: Fix #11121: Simultaneous definition of term and notation in custom
 grammar

---
 test-suite/bugs/closed/bug_11121.v | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_11121.v

(limited to 'test-suite/bugs')

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.
-- 
cgit v1.2.3