1 files changed, 6 insertions, 0 deletions
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 872a6c905..07f24583e 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -7,14 +7,19 @@ Sign
 Cbytecodes
 Copcodes
 Cemitcodes
+Nativevalues
 Declarations
 Retroknowledge
 Pre_env
 Cbytegen
+Nativelambda
+Nativecode
+Nativelib
 Environ
 Conv_oracle
 Closure
 Reduction
+Nativeconv
 Type_errors
 Modops
 Inductive
@@ -24,6 +29,7 @@ Cooking
 Term_typing
 Subtyping
 Mod_typing
+Nativelibrary
 Safe_typing
 
 Vm