diff options
| author | Regis-Gianas | 2014-11-04 22:50:00 +0100 |
|---|---|---|
| committer | Regis-Gianas | 2014-11-04 22:51:36 +0100 |
| commit | d1569f060a114b113ea9f326f1dec1c1e3f101dc (patch) | |
| tree | 68f4bfa95c003264511755ff266230ecefdd5e0d /kernel | |
| parent | 5076e90f880cdc3f085dd8d24f4722d0501d2518 (diff) | |
printing/Ppannotation: New annotation for tactic syntactic objects.
printing/Pptactic: Tag tactics pretty-printing.
printing/Ppvernac: Use the relevent Pptactic pretty-printer.
printing/RichPrinter: Publish two new services.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions