summaryrefslogtreecommitdiff
path: root/src/value.ml
diff options
context:
space:
mode:
authorJon French2018-04-23 17:10:55 +0100
committerJon French2018-05-01 16:54:54 +0100
commitfca88463c50ec7d27dc2670972f13a6015905f64 (patch)
tree410640f80a3760dc31a5dd8a2f887e396c7b6fab /src/value.ml
parent14510c80fa9d105ab61f0ecfb96ea89f7edf6587 (diff)
starting to also do integer support
Diffstat (limited to 'src/value.ml')
-rw-r--r--src/value.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/value.ml b/src/value.ml
index 4848721d..1365b835 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -192,7 +192,7 @@ let value_string_drop = function
| _ -> failwith "value string_drop"
let value_string_length = function
- | [v] -> V_int (coerce_string v |> Sail_lib.string_length |> Big_int.of_int)
+ | [v] -> V_int (coerce_string v |> Sail_lib.string_length)
| _ -> failwith "value string_length"
let value_length = function