aboutsummaryrefslogtreecommitdiff
path: root/kernel/kernel.mllib
diff options
context:
space:
mode:
authorMaxime Dénès2019-11-01 15:53:30 +0100
committerMaxime Dénès2019-11-01 15:53:30 +0100
commitfdabd4dbd6bfd60ad46fc8c945ed063860498e53 (patch)
tree01edf91f8b536ad4acfbba39e114daa06b40f3f8 /kernel/kernel.mllib
parentd00c0b93ec4cb5ca48a9dc2ddf2cfd2038208ee2 (diff)
parentacdaab2a8c2ccb63df364bb75de8a515b2cef484 (diff)
Merge PR #9867: Add primitive floats (binary64 floating-point numbers)
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: ejgallego Reviewed-by: maximedenes Ack-by: proux01 Ack-by: silene Ack-by: vbgl
Diffstat (limited to 'kernel/kernel.mllib')
-rw-r--r--kernel/kernel.mllib1
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 20e742d7f8..2b83c2d868 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -1,6 +1,7 @@
Names
TransparentState
Uint63
+Float64
CPrimitives
Univ
UGraph