aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/pp.ml
diff options
context:
space:
mode:
Diffstat (limited to 'lib/pp.ml')
-rw-r--r--lib/pp.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/lib/pp.ml b/lib/pp.ml
index 5a38b08c3..71c72baa9 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -236,7 +236,7 @@ let rec pr_com ft s =
Format.pp_print_as ft (utf8_length s1) s1;
match os with
Some s2 ->
- if String.length s2 = 0 then (com_eol := true)
+ if Int.equal (String.length s2) 0 then (com_eol := true)
else
(Format.pp_force_newline ft (); pr_com ft s2)
| None -> ()
@@ -441,14 +441,14 @@ let pr_vertical_list pr = function
let prvecti_with_sep sep elem v =
let rec pr i =
- if i = 0 then
+ if Int.equal i 0 then
elem 0 v.(0)
else
let r = pr (i-1) and s = sep () and e = elem i v.(i) in
r ++ s ++ e
in
let n = Array.length v in
- if n = 0 then mt () else pr (n - 1)
+ if Int.equal n 0 then mt () else pr (n - 1)
(* [prvecti pr [|a0 ; ... ; an|]] outputs [pr 0 a0 ++ ... ++ pr n an] *)