diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/rtree.ml | 4 | ||||
| -rw-r--r-- | lib/util.ml | 4 | ||||
| -rw-r--r-- | lib/util.mli | 2 |
3 files changed, 5 insertions, 5 deletions
diff --git a/lib/rtree.ml b/lib/rtree.ml index b1c9345064..e7934c45e4 100644 --- a/lib/rtree.ml +++ b/lib/rtree.ml @@ -173,11 +173,11 @@ let rec pp_tree prl t = | Node(lab,[||]) -> hov 2 (str"("++prl lab++str")") | Node(lab,v) -> hov 2 (str"("++prl lab++str","++brk(1,0)++ - Util.prvect_with_sep Util.pr_coma (pp_tree prl) v++str")") + Util.prvect_with_sep Util.pr_comma (pp_tree prl) v++str")") | Rec(i,v) -> if Array.length v = 0 then str"Rec{}" else if Array.length v = 1 then hov 2 (str"Rec{"++pp_tree prl v.(0)++str"}") else hov 2 (str"Rec{"++int i++str","++brk(1,0)++ - Util.prvect_with_sep Util.pr_coma (pp_tree prl) v++str"}") + Util.prvect_with_sep Util.pr_comma (pp_tree prl) v++str"}") diff --git a/lib/util.ml b/lib/util.ml index 42cdc2bf2c..ea5da9e3c2 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -1194,7 +1194,7 @@ let pr_spc = spc let pr_fnl = fnl let pr_int = int let pr_str = str -let pr_coma () = str "," ++ spc () +let pr_comma () = str "," ++ spc () let pr_semicolon () = str ";" ++ spc () let pr_bar () = str "|" ++ spc () let pr_arg pr x = spc () ++ pr x @@ -1242,7 +1242,7 @@ let rec pr_sequence elem = function let pr_enum pr l = let c,l' = list_sep_last l in - prlist_with_sep pr_coma pr l' ++ + prlist_with_sep pr_comma pr l' ++ (if l'<>[] then str " and" ++ spc () else mt()) ++ pr c let pr_vertical_list pr = function diff --git a/lib/util.mli b/lib/util.mli index 43dd439131..8c811d4390 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -316,7 +316,7 @@ val pr_spc : unit -> std_ppcmds val pr_fnl : unit -> std_ppcmds val pr_int : int -> std_ppcmds val pr_str : string -> std_ppcmds -val pr_coma : unit -> std_ppcmds +val pr_comma : unit -> std_ppcmds val pr_semicolon : unit -> std_ppcmds val pr_bar : unit -> std_ppcmds val pr_arg : ('a -> std_ppcmds) -> 'a -> std_ppcmds |