diff options
Diffstat (limited to 'kernel/nativevalues.ml')
| -rw-r--r-- | kernel/nativevalues.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index 8093df3044..7ffb48221b 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -200,7 +200,7 @@ let mk_block tag args = (* Two instances of dummy_value should not be pointer equal, otherwise comparing them as terms would succeed *) let dummy_value : unit -> t = - fun () _ -> anomaly ~label:"native" (Pp.str "Evaluation failed") + fun () _ -> anomaly ~label:"native" (Pp.str "Evaluation failed.") let cast_accu v = (Obj.magic v:accumulator) @@ -334,6 +334,7 @@ let l_or accu x y = if is_int x && is_int y then no_check_l_or x y else accu x y +[@@@ocaml.warning "-37"] type coq_carry = | Caccu of t | C0 of t @@ -430,7 +431,7 @@ let addmuldiv accu x y z = if is_int x && is_int y && is_int z then no_check_addmuldiv x y z else accu x y z - +[@@@ocaml.warning "-34"] type coq_bool = | Baccu of t | Btrue @@ -491,12 +492,12 @@ let str_encode expr = let str_decode s = let mshl_expr_len = String.length s / 2 in let mshl_expr = Buffer.create mshl_expr_len in - let buf = String.create 2 in + let buf = Bytes.create 2 in for i = 0 to mshl_expr_len - 1 do - String.blit s (2*i) buf 0 2; - Buffer.add_char mshl_expr (bin_of_hex buf) + Bytes.blit_string s (2*i) buf 0 2; + Buffer.add_char mshl_expr (bin_of_hex (Bytes.to_string buf)) done; - Marshal.from_string (Buffer.contents mshl_expr) 0 + Marshal.from_bytes (Buffer.to_bytes mshl_expr) 0 (** Retroknowledge, to be removed when we switch to primitive integers *) |