aboutsummaryrefslogtreecommitdiff
path: root/toplevel
diff options
context:
space:
mode:
authorMaxime Dénès2017-02-15 13:58:45 +0100
committerMaxime Dénès2017-02-15 13:58:45 +0100
commit0df095ec0715f548180bbff70a6feb673c6726a6 (patch)
treed5518ea65638cc486aeeb652530b725925e96d98 /toplevel
parent4fd59386e7f60d16bfe9858c372b354d422ac0b6 (diff)
parent3cdcad29ee9d28b0cb39740004da90a0fe291543 (diff)
Merge PR#314: Miscellaneous fixes for Ocaml warnings.
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/vernac.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 0e72a044c1..c1a659c38d 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -105,7 +105,7 @@ let verbose_phrase verbch loc =
match verbch with
| Some ch ->
let len = snd loc - fst loc in
- let s = String.create len in
+ let s = Bytes.create len in
seek_in ch (fst loc);
really_input ch s 0 len;
Feedback.msg_notice (str s)
@@ -162,7 +162,7 @@ let pr_new_syntax po loc chan_beautify ocom =
let pp_cmd_header loc com =
let shorten s = try (String.sub s 0 30)^"..." with _ -> s in
let noblank s =
- for i = 0 to String.length s - 1 do
+ for i = 0 to Bytes.length s - 1 do
match s.[i] with
| ' ' | '\n' | '\t' | '\r' -> s.[i] <- '~'
| _ -> ()