summaryrefslogtreecommitdiff
path: root/aarch64
diff options
context:
space:
mode:
Diffstat (limited to 'aarch64')
-rw-r--r--aarch64/aarch64_extras.lem2
-rw-r--r--aarch64/mono/aarch64_extras.lem4
2 files changed, 1 insertions, 5 deletions
diff --git a/aarch64/aarch64_extras.lem b/aarch64/aarch64_extras.lem
index a8bc6431..d22ece00 100644
--- a/aarch64/aarch64_extras.lem
+++ b/aarch64/aarch64_extras.lem
@@ -58,8 +58,6 @@ let hex_slice v len lo =
| Nothing -> Fail "hex_slice"
end
-let internal_pick vs = return (head vs)
-
(* Use constants for undefined values for now *)
let undefined_string () = return ""
let undefined_unit () = return ()
diff --git a/aarch64/mono/aarch64_extras.lem b/aarch64/mono/aarch64_extras.lem
index 1e91dd31..ffc8baf0 100644
--- a/aarch64/mono/aarch64_extras.lem
+++ b/aarch64/mono/aarch64_extras.lem
@@ -61,9 +61,7 @@ let hex_slice v len lo =
val BigEndianReverse : forall 'rv 'n 'e. Size 'n => mword 'n -> monad 'rv (mword 'n) 'e
let BigEndianReverse w = return (reverse_endianness w)
-let internal_pick vs = return (head vs)
-
-(* Use constants for undefined values for now *)
+(* Use constants for some undefined values for now *)
let undefined_string () = return ""
let undefined_unit () = return ()
let undefined_int () = return (0:ii)