aboutsummaryrefslogtreecommitdiff
path: root/kernel/kernel.mllib
diff options
context:
space:
mode:
authorMaxime Dénès2014-04-07 15:45:33 -0400
committerMaxime Dénès2014-04-09 01:05:48 -0400
commit2e8c02d5644e8e8e446ab6dfd832322276e44f89 (patch)
tree9f7564ac88d210611cbd5fa5cf2de8efad038e36 /kernel/kernel.mllib
parenta91518d0b07b9a2cd7d9381044c20365771ec382 (diff)
Machine arithmetic operations for native compiler.
This completes the port of the native compiler to retroknowledge. However, some testing and optimizations are still to be done.
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 3267b7e75e..0d0adf9a7d 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -13,6 +13,7 @@ Cbytecodes
Copcodes
Cemitcodes
Nativevalues
+Primitives
Nativeinstr
Opaqueproof
Declareops