aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--kernel/kernel.mllib1
-rw-r--r--lib/clib.mllib1
2 files changed, 0 insertions, 2 deletions
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index f7220c94a1..1e132e3ab2 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -15,7 +15,6 @@ Copcodes
Cemitcodes
Nativevalues
Primitives
-Nativeinstr
Opaqueproof
Declareops
Retroknowledge
diff --git a/lib/clib.mllib b/lib/clib.mllib
index 95007c52ab..1e33173ee1 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -29,7 +29,6 @@ Util
Stateid
Pp
Ppstyle
-Xml_datatype
Richpp
Feedback
CUnix