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

---
 vernac/metasyntax.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac')

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