From 03a50923af6fec0deb0c3c2218656bfb74341e47 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 10 Jan 2019 23:24:28 +0100
Subject: Fixing #9329 (registering empty levels in the order they are
 recomputed).

Was raising an anomaly 'Failure("Grammar.extend")' otherwise.
---
 test-suite/bugs/closed/bug_9329.v | 12 ++++++++++++
 1 file changed, 12 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_9329.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/bug_9329.v b/test-suite/bugs/closed/bug_9329.v
new file mode 100644
index 0000000000..c0322dec40
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9329.v
@@ -0,0 +1,12 @@
+(* Declare empty levels in the same order they are computed *)
+
+Notation "< a ; b ; c >1" :=
+  (sum a (sum b c)) (at level 18, a at level 19, b at level 20, c at level 21).
+Notation "< a ; b ; c >2" :=
+  (sum a (sum b c)) (at level 28, a at level 29, c at level 32, b at level 31).
+Notation "< a ; b ; c >3" :=
+  (sum a (sum b c)) (at level 38, c at level 42, a at level 39, b at level 41).
+Notation "< a ; b ; c >4" :=
+  (sum a (sum b c)) (at level 48, c at level 52, b at level 51, a at level 49).
+Notation "< a ; b >" :=
+  (sum a b) (at level 61, a at level 63, b at level 62).
-- 
cgit v1.2.3