From 44ec3c8fd02f27d1dc7123bfbe5f5018937d6b86 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 25 Dec 2019 13:57:00 +0100
Subject: Fixes #11331 (unexpected level collisions between custom entries and
 constr).

There was a collision at the time of interpreting subentries (in
metasyntax.ml) but also at the time of "optimizing" the entries (in
egramcoq.ml).

Also fixes #9517, fixes #9519, fixes #9640 (part 3).
---
 test-suite/bugs/closed/bug_9517.v | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_9517.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/bug_9517.v b/test-suite/bugs/closed/bug_9517.v
new file mode 100644
index 0000000000..bb43edbe74
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9517.v
@@ -0,0 +1,19 @@
+Declare Custom Entry expr.
+Declare Custom Entry stmt.
+Notation "x" := x (in custom stmt, x ident).
+Notation "x" := x (in custom expr, x ident).
+
+Notation "1" := 1 (in custom expr).
+
+Notation "! x = y !" := (pair x y) (in custom stmt at level 0, x custom expr, y custom expr).
+Notation "? x = y" := (pair x y) (in custom stmt at level 0, x custom expr, y custom expr).
+Notation "x = y" := (pair x y) (in custom stmt at level 0, x custom expr, y custom expr).
+
+Notation "stmt:( s )" := s (s custom stmt).
+Check stmt:(! _ = _ !).
+Check stmt:(? _ = _).
+Check stmt:(_ = _).
+Check stmt:(! 1 = 1 !).
+Check stmt:(? 1 = 1).
+Check stmt:(1 = 1).
+Check stmt:(_ = 1).
-- 
cgit v1.2.3