diff options
| author | Regis-Gianas | 2014-10-30 18:48:22 +0100 |
|---|---|---|
| committer | Regis-Gianas | 2014-11-04 22:51:35 +0100 |
| commit | 00bb36da0696b1442bf4e0bb1a657e3de8c92b1e (patch) | |
| tree | 4c1465b0b6fc6093dff8f21da83ae509d6e671b6 /lib | |
| parent | 7f40ab12d4ff5ecceccbeb72555e7c4421bd9dd0 (diff) | |
printing/Ppconstr.Make:
- Functorize Ppconstr with respect to a set of tagging functions.
- These functions are meant to introduce tags to produce semistructured
pretty printings.
printing/Ppconstr:
Preserve the previous behaviour of this module by instantiating Make
with tagging functions that do nothing.
Diffstat (limited to 'lib')
0 files changed, 0 insertions, 0 deletions