diff options
| author |  Regis-Gianas <yrg@pps.univ-paris-diderot.fr> | 2014-11-04 12:05:53 +0100 |
|---|---|---|
| committer | Regis-Gianas <yrg@pps.univ-paris-diderot.fr> | 2014-11-04 22:51:36 +0100 |
| commit | d6b6deb1cb02dca80349aa30221ea8569e72d9da (patch) | |
| tree | 3749d972a8257aa7db77134f0f420bbd9f18a372 /printing/printing.mllib | |
| parent | 970725685ee7ecb03fa071e94695988f2b14bd90 (diff) | |
printing/RichPrinter: New API for rich pretty-printing.
printing/Ppannotation: Define the projection of annotations into XML attributes.
lib/richPp: Implements valid entities escaping.
Diffstat (limited to 'printing/printing.mllib')
| -rw-r--r-- | printing/printing.mllib | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/printing/printing.mllib b/printing/printing.mllib index 01c835d89..713c2dee6 100644 --- a/printing/printing.mllib +++ b/printing/printing.mllib @@ -9,3 +9,4 @@ Printmod Prettyp Ppvernac Ppvernacsig +RichPrinter |