From b02ae8e4faa26ded157c9379572e9a43e0394290 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 9 Mar 2020 14:39:35 +0100
Subject: Fix #11730: Mangle Names vs Infix

---
 test-suite/bugs/closed/bug_11730.v | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_11730.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/bug_11730.v b/test-suite/bugs/closed/bug_11730.v
new file mode 100644
index 0000000000..f788636f9c
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11730.v
@@ -0,0 +1,6 @@
+Set Mangle Names.
+
+Infix "&&&" := andb (at level 40, left associativity).
+(* Error: Variable _0 occurs more than once. *)
+
+Check (_ &&& _).
-- 
cgit v1.2.3