From 5f1270242f71a0a1da7c868967e1071d28ed83fb Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Tue, 28 Aug 2018 23:37:49 +0200
Subject: Add next_{up,down} primitive float functions

---
 kernel/primred.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'kernel/primred.ml')

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
-- 
cgit v1.2.3