diff options
Diffstat (limited to 'kernel/primred.ml')
| -rw-r--r-- | kernel/primred.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/kernel/primred.ml b/kernel/primred.ml index cfe6c8effe..2766793005 100644 --- a/kernel/primred.ml +++ b/kernel/primred.ml @@ -302,6 +302,10 @@ struct let f = get_float evd args 0 in let e = get_int evd args 1 in E.mkFloat env (Float64.ldshiftexp f e) + | Float64next_up -> + let f = get_float1 evd args in E.mkFloat env (Float64.next_up f) + | Float64next_down -> + let f = get_float1 evd args in E.mkFloat env (Float64.next_down f) let red_prim env evd p args = try |