diff options
| author | Regis-Gianas | 2014-11-04 14:50:06 +0100 |
|---|---|---|
| committer | Regis-Gianas | 2014-11-04 22:51:36 +0100 |
| commit | 678b17b52b0b59a5470d8272474e692b2fe023e3 (patch) | |
| tree | 9cae63a5e14dea376ce82c16643aeb110c95eddb /kernel | |
| parent | db9b17d55f539fcfda799a9fe15caa2530cc727f (diff) | |
lib/Pp.tag: New.
A combinator to introduce tags.
printing/{Ppconstr, Ppvernac}: Use it.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions