diff options
| author | Hugo Herbelin | 2017-11-07 16:26:21 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2017-11-24 18:08:05 +0100 |
| commit | be133d7bc92b67a6581a99f7aa679fb3a60ce57b (patch) | |
| tree | 2b0f757e0e0da637bfa96d2f94875aa8987c71f1 /kernel | |
| parent | 1161ccf74578c3190d296dc37f39edecf28cf078 (diff) | |
Extending further PR#6047 (system to register printers for Ltac values).
We generalize the possible use of levels to raw and glob printers.
This is potentially useful for printing ltac expressions which are the
glob level.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions