diff options
| author | Regis-Gianas | 2014-10-30 22:14:22 +0100 |
|---|---|---|
| committer | Regis-Gianas | 2014-11-04 22:51:35 +0100 |
| commit | 0aa24d51d2606549da87ed42085f612f2dbb1428 (patch) | |
| tree | 292fc331cbfe420873eb9e1e661cc5c879aeba3d /lib/lib.mllib | |
| parent | 812c611bdc8532b7cd25d9368a8356be3eb1d34a (diff) | |
RichPp: New module.
It is responsible for turning a tagged pretty-printing into
a semi-structured document.
clib.mllib: Include RichPp as well as Xml_*.
The migration of Xml_* from lib to clib is needed by RichPp
depends on these modules.
Diffstat (limited to 'lib/lib.mllib')
| -rw-r--r-- | lib/lib.mllib | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/lib/lib.mllib b/lib/lib.mllib index b5421a8c89..f3f6ad8fc7 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -1,6 +1,3 @@ -Xml_lexer -Xml_parser -Xml_printer Errors Bigint Dyn |