diff options
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 (**********************************************************************) |