diff options
| author |  Regis-Gianas <yrg@pps.univ-paris-diderot.fr> | 2014-11-04 14:46:47 +0100 |
|---|---|---|
| committer | Regis-Gianas <yrg@pps.univ-paris-diderot.fr> | 2014-11-04 22:51:36 +0100 |
| commit | db9b17d55f539fcfda799a9fe15caa2530cc727f (patch) | |
| tree | 112ce79b5bff93308caff927f138fd2768dde5be /tactics | |
| parent | 7b3f2d2783f74a38b4fe40d2dc5f58b8d5bae0f1 (diff) | |
printing/Ppannotation: Introduce a new annotation for keywords.
printing/{Ppconstr, Ppvernac}: Use it.
Diffstat (limited to 'tactics')
0 files changed, 0 insertions, 0 deletions