From 354cf4233194e948a4630bf180643974017dc342 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 13 May 2020 17:33:27 +0200
Subject: Tests for bugs #9583 (fixed by #11613) and #9679.

---
 test-suite/bugs/closed/bug_9583.v | 7 +++++++
 test-suite/bugs/closed/bug_9679.v | 6 ++++++
 2 files changed, 13 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_9583.v
 create mode 100644 test-suite/bugs/closed/bug_9679.v

diff --git a/test-suite/bugs/closed/bug_9583.v b/test-suite/bugs/closed/bug_9583.v
new file mode 100644
index 0000000000..14232e8578
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9583.v
@@ -0,0 +1,7 @@
+(* Was causing a stack overflow before #11613 *)
+Declare Custom Entry bla.
+Notation "[ t ]" := (t) (at level 0, t custom bla at level 0).
+Notation "] t [" := (t) (in custom bla at level 0, t custom bla at level 0).
+Notation "t" := (t) (in custom bla at level 0, t constr at level 9).
+Notation "0" := (0) (in custom bla at level 0).
+Check fun x => [ ] x [ ].
diff --git a/test-suite/bugs/closed/bug_9679.v b/test-suite/bugs/closed/bug_9679.v
new file mode 100644
index 0000000000..24e69d23f9
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9679.v
@@ -0,0 +1,6 @@
+(* Was raising an anomaly *)
+Notation "'[#' ] f '|' x .. z '=n>' b" :=
+  (fun x => .. (fun z => f b) ..)
+    (at level 201, x binder, z binder,
+     format "'[  ' [# ] '[' f  | ']'  x  ..  z  =n>  '[' b ']' ']'"
+    ).
-- 
cgit v1.2.3