aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/printmod.mli
Commit message (Expand)AuthorAge
* Split off Universes functions dealing with names.Gravatar Gaëtan Gilbert2018-05-17
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* [ast] Improve precision of Ast location recognition in serialization.Gravatar Emilio Jesus Gallego Arias2018-02-22
* Allow local universe renaming in Print.Gravatar Gaëtan Gilbert2017-11-25
* [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* [pp] Remove unused printing tagging infrastructure.Gravatar Emilio Jesus Gallego Arias2017-03-21
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* Adding rich-printing facilities to Printmod.Gravatar Pierre-Marie Pédrot2014-11-19
* Dir_path --> DirPathGravatar letouzey2013-02-19
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Updating headers.Gravatar herbelin2012-08-08
* place all pretty-printing files in new dir printing/Gravatar letouzey2012-05-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-04 03:27:08 +0000