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 ++++++
 vernac/metasyntax.ml               | 2 +-
 2 files changed, 7 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/bug_11730.v

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 (_ &&& _).
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 33fd14a731..10946d78f0 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1708,7 +1708,7 @@ let add_infix ~local deprecation env ({CAst.loc;v=inf},modifiers) pr sc =
   (* check the precedence *)
   let vars = names_of_constr_expr pr in
   let x = Namegen.next_ident_away (Id.of_string "x") vars in
-  let y = Namegen.next_ident_away (Id.of_string "y") vars in
+  let y = Namegen.next_ident_away (Id.of_string "y") (Id.Set.add x vars) in
   let metas = [inject_var x; inject_var y] in
   let c = mkAppC (pr,metas) in
   let df = CAst.make ?loc @@ Id.to_string x ^" "^(quote_notation_token inf)^" "^Id.to_string y in
-- 
cgit v1.2.3