aboutsummaryrefslogtreecommitdiff
path: root/lib/ppstyle.mli
AgeCommit message (Expand)Author
2017-03-21[pp] Move terminal-specific tagging to the toplevel.Emilio Jesus Gallego Arias
2017-03-21[pp] Remove special tag type and handler from Pp.Emilio Jesus Gallego Arias
2017-03-21[pp] Replace `Pp.Tag` by `Ppstyle.tag` = `string list`Emilio Jesus Gallego Arias
2016-09-30[pp] Remove duplicate color logger.Emilio Jesus Gallego Arias
2016-06-29A new infrastructure for warnings.Maxime Dénès
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-01-20Update copyright headers.Maxime Dénès
2015-06-25Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.Thomas Sibut-Pinote