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).

3 files changed, 31 insertions, 0 deletions

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).
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index f65696e464..807914a671 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -71,3 +71,7 @@ The command has indeed failed with message:
 The format is not the same on the right- and left-hand sides of the special token "..".
 The command has indeed failed with message:
 The format is not the same on the right- and left-hand sides of the special token "..".
+Entry constr:expr is
+[ "201" RIGHTA
+  [ "{"; constr:operconstr LEVEL "200"; "}" ] ]
+
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 4de6ce19b4..2906698386 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -184,3 +184,11 @@ Fail Notation " {@ T1 ; T2 ; .. ; Tn } " :=
   (format "'[v' {@  '[' T1 ']'  ;  '//' '['  T2  ']'   ;  '//' ..  ;   '//' '['  Tn  ']'  } ']'").
 
 End M.
+
+Module Bug11331.
+
+Declare Custom Entry expr.
+Notation "{ p }" := (p) (in custom expr at level 201, p constr).
+Print Custom Grammar expr.
+
+End Bug11331.