1 files changed, 18 insertions, 5 deletions
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 8c1dd53a..29fe887d 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -1,32 +1,45 @@
 Names
+Uint31
 Univ
 Esubst
+Sorts
+Evar
+Constr
+Context
+Vars
 Term
 Mod_subst
-Sign
 Cbytecodes
 Copcodes
 Cemitcodes
-Declarations
+Nativevalues
+Primitives
+Nativeinstr
+Opaqueproof
+Declareops
 Retroknowledge
+Conv_oracle
 Pre_env
 Cbytegen
+Nativelambda
+Nativecode
+Nativelib
 Environ
-Conv_oracle
 Closure
 Reduction
+Nativeconv
 Type_errors
-Entries
 Modops
 Inductive
 Typeops
+Fast_typeops
 Indtypes
 Cooking
 Term_typing
 Subtyping
 Mod_typing
+Nativelibrary
 Safe_typing
-
 Vm
 Csymtable
 Vconv