diff options
| author |  Regis-Gianas <yrg@pps.univ-paris-diderot.fr> | 2014-11-04 21:51:25 +0100 |
|---|---|---|
| committer | Regis-Gianas <yrg@pps.univ-paris-diderot.fr> | 2014-11-04 22:51:36 +0100 |
| commit | fa6d5dd5efed2fe1f732d61eac126e39fef38305 (patch) | |
| tree | 8e8d8b8e3655d238a871ba5d667428dfdc343f26 /printing/printing.mllib | |
| parent | af0325ee57fad526be8f3afab5335faaf82cb0c8 (diff) | |
printing/Pptacticsig: New signature for tactic pretty-printers.
printing/Pptactic: Use it.
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 713c2dee6..791070298 100644 --- a/printing/printing.mllib +++ b/printing/printing.mllib @@ -5,6 +5,7 @@ Ppconstr Ppconstrsig Printer Pptactic +Pptacticsig Printmod Prettyp Ppvernac |