Merge PR #11311: Fix handling of recursive notations with custom entries

Reviewed-by: herbelin

2 files changed, 21 insertions, 0 deletions

diff --git a/test-suite/bugs/bug_9490.v b/test-suite/bugs/bug_9490.v
new file mode 100644
index 0000000000..a5def40c49
--- /dev/null
+++ b/test-suite/bugs/bug_9490.v
@@ -0,0 +1,9 @@
+Declare Custom Entry with_pattern.
+Declare Custom Entry M_branch.
+Notation "'with' | p1 | .. | pn 'end'" :=
+  (cons p1 (.. (cons pn nil) ..))
+  (in custom with_pattern at level 91, p1 custom M_branch at level 202, pn custom M_branch at level 202).
+Notation "'bla'" := I (in custom M_branch at level 202).
+Notation "'[use_with'  l  ]" := (l) (at level 0, l custom with_pattern at level 91).
+Check [use_with with | bla end].
+Check [use_with with | bla | bla end].
diff --git a/test-suite/bugs/bug_9532.v b/test-suite/bugs/bug_9532.v
new file mode 100644
index 0000000000..d198d45f2f
--- /dev/null
+++ b/test-suite/bugs/bug_9532.v
@@ -0,0 +1,12 @@
+Declare Custom Entry atom.
+Notation "1" := tt (in custom atom).
+Notation "atom:( s )" := s (s custom atom).
+
+Declare Custom Entry expr.
+Notation "expr:( s )" := s (s custom expr).
+Notation "( x , y , .. , z )" :=  (@cons unit x (@cons unit y .. (@cons unit z (@nil unit)) ..))
+  (in custom expr at level 0, x custom atom, y custom atom, z custom atom).
+
+Check atom:(1).
+Check expr:((1,1)).
+Check expr:((1,1,1)).