aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-06-01 02:37:15 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-06-12 14:42:28 +0200
commit615290d0f9d5cad7c508d45cf4ab89aecff033b2 (patch)
treef5db022987df54435d807017f4f647ca9e275e9c /library
parent4aaeb5d429227505adfde9fe04c3c0fb69f2d37f (diff)
[api] Remove Misctypes.
We move the last 3 types to more adequate places.
Diffstat (limited to 'library')
-rw-r--r--library/library.mllib1
1 files changed, 0 insertions, 1 deletions
diff --git a/library/library.mllib b/library/library.mllib
index 1c0368847..2ac4266fc 100644
--- a/library/library.mllib
+++ b/library/library.mllib
@@ -6,7 +6,6 @@ Nametab
Global
Decl_kinds
Lib
-Misctypes
Declaremods
Loadpath
Library