diff options
| author | Hugo Herbelin | 2018-12-16 20:33:09 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2018-12-18 18:24:31 +0100 |
| commit | 4e529454022b7d2dc0c57d29c813c5801dfd438c (patch) | |
| tree | d84962c9f9dd70977f3f151610b9c4769ac2023e /vernac | |
| parent | 4c733a9282bf2a272eb0ff48811b528aebbfb5a0 (diff) | |
Fixes #9229 (Infix not robust wrt choice of variable names).
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/metasyntax.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 4e79b50b79..3da12e7714 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1563,14 +1563,17 @@ let add_notation_extra_printing_rule df k v = (* Infix notations *) -let inject_var x = CAst.make @@ CRef (qualid_of_ident (Id.of_string x),None) +let inject_var x = CAst.make @@ CRef (qualid_of_ident x,None) let add_infix local env ({CAst.loc;v=inf},modifiers) pr sc = check_infix_modifiers modifiers; (* check the precedence *) - let metas = [inject_var "x"; inject_var "y"] in + 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 metas = [inject_var x; inject_var y] in let c = mkAppC (pr,metas) in - let df = CAst.make ?loc @@ "x "^(quote_notation_token inf)^" y" in + let df = CAst.make ?loc @@ Id.to_string x ^" "^(quote_notation_token inf)^" "^Id.to_string y in add_notation local env c (df,modifiers) sc (**********************************************************************) |