From 6070a0775d61a1551b8e2c1ca2ff7e39f2ba32f4 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Thu, 31 Jan 2019 14:41:47 +0000
Subject: Adapt HOL library to monad changes

---
 lib/hol/sail2_prompt_monad.lem | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'lib')

diff --git a/lib/hol/sail2_prompt_monad.lem b/lib/hol/sail2_prompt_monad.lem
index 3af931a5..5f0f7478 100644
--- a/lib/hol/sail2_prompt_monad.lem
+++ b/lib/hol/sail2_prompt_monad.lem
@@ -34,16 +34,17 @@ let inline try_catchR = try_catchRS
 
 let inline maybe_fail = maybe_failS
 
+let inline read_memt_bytes = read_memt_bytesS
 let inline read_mem_bytes = read_mem_bytesS
 let inline read_reg = read_regS
 let inline reg_deref = read_regS
+let inline read_memt = read_memtS
 let inline read_mem = read_memS
-let inline read_tag = read_tagS
 let inline excl_result = excl_resultS
 let inline write_reg = write_regS
-let inline write_tag = write_tagS
-let inline write_mem_ea wk addr sz = write_mem_eaS wk addr (nat_of_int sz)
-let inline write_mem_val = write_mem_valS
+let inline write_mem_ea wk addr sz = return ()
+let inline write_memt = write_memtS
+let inline write_mem = write_memS
 let barrier _ = return ()
 
 let inline assert_exp = assert_expS
-- 
cgit v1.2.3