Merge branch 'sail2' into rmem_interpreter

2 files changed, 4 insertions, 10 deletions

diff --git a/aarch64/aarch64_extras.lem b/aarch64/aarch64_extras.lem
index d22ece00..b662e230 100644
--- a/aarch64/aarch64_extras.lem
+++ b/aarch64/aarch64_extras.lem
@@ -78,7 +78,7 @@ val write_ram : forall 'rv 'e.
   integer -> integer -> list bitU -> list bitU -> list bitU -> monad 'rv unit 'e
 let write_ram addrsize size hexRAM address value =
   write_mem_ea Write_plain address size >>
-  write_mem_val value >>= fun _ ->
+  write_mem Write_plain address size value >>= fun _ ->
   return ()
 
 val read_ram : forall 'rv 'e.
diff --git a/aarch64/prelude.sail b/aarch64/prelude.sail
index f4f7dc75..431ad1f7 100755
--- a/aarch64/prelude.sail
+++ b/aarch64/prelude.sail
@@ -284,17 +284,11 @@ val abs_real = {coq: "Rabs", _: "abs_real"} : real -> real
 
 overload abs = {abs_atom, abs_real}
 
-val quotient_nat = {ocaml: "quotient", lem: "integerDiv", c: "tdiv_int"} : (nat, nat) -> nat
-
 val quotient_real = {ocaml: "quotient_real", lem: "realDiv", c: "div_real", coq: "Rdiv"} : (real, real) -> real
 
-val quotient = {ocaml: "quotient", lem: "integerDiv", c: "tdiv_int", coq: "Z.quot"} : (int, int) -> int
-
-overload operator / = {quotient_nat, quotient, quotient_real}
-
-val modulus = {ocaml: "modulus", lem: "hardware_mod", c: "tmod_int", coq: "Z.rem"} : (int, int) -> int
-
-overload operator % = {modulus}
+overload operator / = {ediv_int, quotient_real}
+overload div = {ediv_int}
+overload operator % = {emod_int}
 
 val Real = {ocaml: "to_real", lem: "realFromInteger", c: "to_real", coq: "IZR"} : int -> real