summaryrefslogtreecommitdiff
path: root/common
diff options
context:
space:
mode:
Diffstat (limited to 'common')
-rw-r--r--common/Values.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/common/Values.v b/common/Values.v
index af242c9..ceff333 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -117,13 +117,13 @@ Definition absf (v: val) : val :=
Definition intoffloat (v: val) : val :=
match v with
- | Vfloat f => Vint (Float.intoffloat f)
+ | Vfloat f => match Float.intoffloat f with Some n => Vint n | None => Vundef end
| _ => Vundef
end.
Definition intuoffloat (v: val) : val :=
match v with
- | Vfloat f => Vint (Float.intuoffloat f)
+ | Vfloat f => match Float.intuoffloat f with Some n => Vint n | None => Vundef end
| _ => Vundef
end.