diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-10-13 13:44:35 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-10-18 21:56:50 +0200 |
| commit | 7ff42d43a6107dff984676902943ec32f187c40d (patch) | |
| tree | 8c488cb2a8752144c3a744203129001bf3a2959e /lib/cErrors.ml | |
| parent | dff1450d43909e8aeaf8ce2db8bc19be42ee1ab1 (diff) | |
[pp] Add tagging function to all low-level printing calls.
The current tag system in `Pp` is generic, which implies we must choose
a tagging function when calling a printer.
For console printing there is a single choice, thus this commits adds it
a few missing cases.
Diffstat (limited to 'lib/cErrors.ml')
0 files changed, 0 insertions, 0 deletions