aboutsummaryrefslogtreecommitdiff
path: root/kernel/cemitcodes.ml
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2019-11-21 15:38:39 +0100
committerEmilio Jesus Gallego Arias2019-11-21 15:38:39 +0100
commitd016f69818b30b75d186fb14f440b93b0518fc66 (patch)
tree32cd948273f79a2c01ad27b4ed0244ea60d7e2f9 /kernel/cemitcodes.ml
parentb680b06b31c27751a7d551d95839aea38f7fbea1 (diff)
[coq] Untabify the whole ML codebase.
We also remove trailing whitespace. Script used: ```bash for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done ```
Diffstat (limited to 'kernel/cemitcodes.ml')
-rw-r--r--kernel/cemitcodes.ml20
1 files changed, 10 insertions, 10 deletions
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 5e82cef810..4e22421f56 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -64,14 +64,14 @@ type patches = {
reloc_infos : (reloc_info * int array) array;
}
-let patch_char4 buff pos c1 c2 c3 c4 =
+let patch_char4 buff pos c1 c2 c3 c4 =
Bytes.unsafe_set buff pos c1;
Bytes.unsafe_set buff (pos + 1) c2;
Bytes.unsafe_set buff (pos + 2) c3;
- Bytes.unsafe_set buff (pos + 3) c4
-
+ Bytes.unsafe_set buff (pos + 3) c4
+
let patch1 buff pos n =
- patch_char4 buff pos
+ patch_char4 buff pos
(Char.unsafe_chr n) (Char.unsafe_chr (n asr 8)) (Char.unsafe_chr (n asr 16))
(Char.unsafe_chr (n asr 24))
@@ -116,9 +116,9 @@ let out_word env b1 b2 b3 b4 =
if len <= Sys.max_string_length / 2
then 2 * len
else
- if len = Sys.max_string_length
- then invalid_arg "String.create" (* Pas la bonne exception .... *)
- else Sys.max_string_length in
+ if len = Sys.max_string_length
+ then invalid_arg "String.create" (* Pas la bonne exception .... *)
+ else Sys.max_string_length in
let new_buffer = Bytes.create new_len in
Bytes.blit env.out_buffer 0 new_buffer 0 len;
env.out_buffer <- new_buffer
@@ -359,9 +359,9 @@ let emit_instr env = function
(* Emission of a current list and remaining lists of instructions. Include some peephole optimization. *)
let rec emit env insns remaining = match insns with
- | [] ->
- (match remaining with
- [] -> ()
+ | [] ->
+ (match remaining with
+ [] -> ()
| (first::rest) -> emit env first rest)
(* Peephole optimizations *)
| Kpush :: Kacc n :: c ->