From 75f5e200f4f7eb6ca829869a8f8dada45e9751e9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 20 Jul 2018 23:37:23 +0200
Subject: Fixing #8106 (anomaly if declaring levels for only printing then only
 parsing).

Notations were not initially designed to support independent parsing
and printing rules. Some redesign of this part of the code shall be
necessary at some time.
---
 test-suite/bugs/closed/8106.v | 4 ++++
 1 file changed, 4 insertions(+)
 create mode 100644 test-suite/bugs/closed/8106.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/8106.v b/test-suite/bugs/closed/8106.v
new file mode 100644
index 0000000000..a711c5adef
--- /dev/null
+++ b/test-suite/bugs/closed/8106.v
@@ -0,0 +1,4 @@
+(* Was raising an anomaly "already assigned a level" on the second line *)
+
+Notation "c1 ; c2" := (c1 + c2) (only printing, at level 76, right associativity, c1 at level 76, c2 at level 76).
+Notation "c1 ; c2" := (c1 + c2) (only parsing, at level 76, right associativity, c2 at level 76).
-- 
cgit v1.2.3