aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--kernel/cemitcodes.ml8
-rw-r--r--tools/coqdoc/index.ml8
2 files changed, 8 insertions, 8 deletions
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index a0a13174ff..f2c3b402b3 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -106,10 +106,10 @@ let extend_label_table needed =
let backpatch (pos, orig) =
let displ = (!out_position - orig) asr 2 in
- !out_buffer.[pos] <- Char.unsafe_chr displ;
- !out_buffer.[pos+1] <- Char.unsafe_chr (displ asr 8);
- !out_buffer.[pos+2] <- Char.unsafe_chr (displ asr 16);
- !out_buffer.[pos+3] <- Char.unsafe_chr (displ asr 24)
+ Bytes.set !out_buffer pos @@ Char.unsafe_chr displ;
+ Bytes.set !out_buffer (pos+1) @@ Char.unsafe_chr (displ asr 8);
+ Bytes.set !out_buffer (pos+2) @@ Char.unsafe_chr (displ asr 16);
+ Bytes.set !out_buffer (pos+3) @@ Char.unsafe_chr (displ asr 24)
let define_label lbl =
if lbl >= Array.length !label_table then extend_label_table lbl;
diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
index c9cb676e98..34108eff42 100644
--- a/tools/coqdoc/index.ml
+++ b/tools/coqdoc/index.ml
@@ -205,17 +205,17 @@ let prepare_entry s = function
while !j <= l do
if not !quoted then begin
(match s.[!j] with
- | '_' -> ntn.[!k] <- ' '; incr k
- | 'x' -> ntn.[!k] <- '_'; incr k
+ | '_' -> Bytes.set ntn !k ' '; incr k
+ | 'x' -> Bytes.set ntn !k '_'; incr k
| '\'' -> quoted := true
| _ -> assert false)
end
else
if s.[!j] = '\'' then
if (!j = l || s.[!j+1] = '_') then quoted := false
- else (incr j; ntn.[!k] <- s.[!j]; incr k)
+ else (incr j; Bytes.set ntn !k s.[!j]; incr k)
else begin
- ntn.[!k] <- s.[!j];
+ Bytes.set ntn !k s.[!j];
incr k
end;
incr j