aboutsummaryrefslogtreecommitdiff
path: root/kernel/kernel.mllib
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/kernel.mllib')
-rw-r--r--kernel/kernel.mllib5
1 files changed, 3 insertions, 2 deletions
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 0b10e788b6..5108744bde 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -1,6 +1,7 @@
Names
TransparentState
-Uint31
+Uint63
+CPrimitives
Univ
UGraph
Esubst
@@ -19,11 +20,11 @@ Opaqueproof
Declarations
Entries
Nativevalues
-CPrimitives
Declareops
Retroknowledge
Conv_oracle
Environ
+Primred
CClosure
Reduction
Clambda