diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/metasyntax.ml | 9 | ||||
| -rw-r--r-- | vernac/ppvernac.ml | 6 | ||||
| -rw-r--r-- | vernac/pvernac.ml | 2 |
3 files changed, 10 insertions, 7 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 (**********************************************************************) diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 8535585749..e0dd3380f9 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -700,7 +700,7 @@ open Pputils | None -> mt() | Some r -> keyword "Eval" ++ spc() ++ - pr_red_expr (pr_constr, pr_lconstr, pr_smart_global, pr_constr) keyword r ++ + Ppred.pr_red_expr (pr_constr, pr_lconstr, pr_smart_global, pr_constr) keyword r ++ keyword " in" ++ spc() in let pr_def_body = function @@ -1134,7 +1134,7 @@ open Pputils let pr_mayeval r c = match r with | Some r0 -> hov 2 (keyword "Eval" ++ spc() ++ - pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r0 ++ + Ppred.pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r0 ++ spc() ++ keyword "in" ++ spc () ++ pr_lconstr c) | None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr c) in @@ -1146,7 +1146,7 @@ open Pputils | VernacDeclareReduction (s,r) -> return ( keyword "Declare Reduction" ++ spc () ++ str s ++ str " := " ++ - pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r + Ppred.pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r ) | VernacPrint p -> return (pr_printable p) diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml index f26e0d0885..a647b2ef73 100644 --- a/vernac/pvernac.ml +++ b/vernac/pvernac.ml @@ -52,4 +52,4 @@ let set_command_entry e = Vernac_.command_entry_ref := e let get_command_entry () = !Vernac_.command_entry_ref let () = - register_grammar Stdarg.wit_red_expr (Vernac_.red_expr); + register_grammar Genredexpr.wit_red_expr (Vernac_.red_expr); |