diff options
| author | Regis-Gianas | 2014-11-04 21:57:36 +0100 |
|---|---|---|
| committer | Regis-Gianas | 2014-11-04 22:51:36 +0100 |
| commit | 5076e90f880cdc3f085dd8d24f4722d0501d2518 (patch) | |
| tree | 9a048b5382d486af51b5cefd9af8a0d461c00368 /kernel | |
| parent | fa6d5dd5efed2fe1f732d61eac126e39fef38305 (diff) | |
printing/Pptactic.Make: New.
- Functorize with respect to the pretty-printer for constr.
- Include the application of Make to Ppconstr at toplevel in order to preserve
previous behavior.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions