aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/ppstyle.mli
Commit message (Expand)AuthorAge
* [pp] Remove duplicate color logger.Gravatar Emilio Jesus Gallego Arias2016-09-30
* A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.Gravatar Thomas Sibut-Pinote2015-06-25