aboutsummaryrefslogtreecommitdiff
path: root/dataType.mli
diff options
context:
space:
mode:
authorSébastien Dailly <sebastien@chimrod.com>2017-11-09 21:43:45 +0100
committerSébastien Dailly <sebastien@chimrod.com>2017-11-09 21:43:45 +0100
commit678bb5c2500be0071117600f23e5a557c39fb403 (patch)
tree8d8210bf9736cb5820fb6b2f83de32cbf6c708a9 /dataType.mli
parent163a82655b1b3649c9bff4db05f487db3a992a40 (diff)
Added some functions
Diffstat (limited to 'dataType.mli')
-rwxr-xr-xdataType.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/dataType.mli b/dataType.mli
index 5397fdb..2589e68 100755
--- a/dataType.mli
+++ b/dataType.mli
@@ -44,6 +44,7 @@ module Num: sig
val abs: t -> t
val floor: t -> t
+ val round_down: t -> t
val gcd: t -> t -> t
val lcm: t -> t -> t