aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/ppvernacsig.mli
Commit message (Collapse)AuthorAge
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Ppvernacsig: New.Gravatar Regis-Gianas2014-11-04
- Define the signature for a pretty-printer of vernacular commands. Ppvernac: Use it.