aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/clib.mllib
diff options
context:
space:
mode:
Diffstat (limited to 'lib/clib.mllib')
-rw-r--r--lib/clib.mllib3
1 files changed, 0 insertions, 3 deletions
diff --git a/lib/clib.mllib b/lib/clib.mllib
index 1e33173ee..c73ae9b90 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -15,7 +15,6 @@ Store
Exninfo
Backtrace
IStream
-Pp_control
Flags
Control
Loc
@@ -28,8 +27,6 @@ CStack
Util
Stateid
Pp
-Ppstyle
-Richpp
Feedback
CUnix
Envars