aboutsummaryrefslogtreecommitdiff
path: root/lib/pp.mli
AgeCommit message (Expand)Author
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-23Fixing typos - Part 3JPR
2019-05-23Fixing typos - Part 2JPR
2018-10-06[api] Remove (most) 8.9 deprecated objects.Emilio Jesus Gallego Arias
2018-07-23Displays the differences between successive proof steps in coqtop and CoqIDE.Jim Fehrle
2018-02-27Update headers following #6543.Théo Zimmermann
2017-12-12Improving spacing in printing disjunctive patterns.Hugo Herbelin
2017-07-27deprecate Pp.std_ppcmds type aliasMatej Košík
2017-07-12format pairs of items for pr_depth to get alternating separatorsPaul Steckler
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-07completing a sentence in a commentMatej Košík
2017-04-05[toplevel] Remove exception error printer in favor of feedback printer.Emilio Jesus Gallego Arias
2017-03-21[pp] Hide the internal representation of `std_ppcmds`.Emilio Jesus Gallego Arias
2017-03-21[pp] [ide] Minor cleanups in pp code.Emilio Jesus Gallego Arias
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] Make feedback the only logging mechanism.Emilio Jesus Gallego Arias
2017-03-21[pp] Remove redundant white spacing pp construct.Emilio Jesus Gallego Arias
2017-03-21[pp] Force well-formed boxes by construction.Emilio Jesus Gallego Arias
2017-03-21[pp] Force well-tagged docs by construction.Emilio Jesus Gallego Arias
2017-03-21[pp] Implement n-ary glue.Emilio Jesus Gallego Arias
2017-03-21[pp] Make pp public to allow serialization.Emilio Jesus Gallego Arias
2017-03-21[pp] Prepare for serialization, remove opaque glue.Emilio Jesus Gallego Arias
2017-03-21[pp] Remove `Pp.stras`.Emilio Jesus Gallego Arias
2017-03-21[pp] Replace `Pp.Tag` by `Ppstyle.tag` = `string list`Emilio Jesus Gallego Arias
2017-02-20Merge PR#189: Remove tabulation support from pretty-printing.Maxime Dénès
2016-10-12Merge PR #224 into v8.6Pierre-Marie Pédrot
2016-10-09Moving Pp.comments to CLexer so that Pp is purer (no more side-effectHugo Herbelin
2016-09-30[pp] Remove duplicate color logger.Emilio Jesus Gallego Arias
2016-06-29A new infrastructure for warnings.Maxime Dénès
2016-06-02Add documentation to the low-level `Pp` functions.Emilio Jesus Gallego Arias
2016-06-02Remove tabulation support from pretty-printing.Guillaume Melquiond
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-05-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-04typoEnrico Tassi
2016-04-09In pr_clauses, do not print a leading space by default so that it canHugo Herbelin
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-09-20Rich printing of messages.Pierre-Marie Pédrot
2015-05-04Add a [Redirect] vernacular commandClément Pit--Claudel
2015-04-23Removing dead code in Pp.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-12-16msg_info now puts infomsg tag in emacs mode.Pierre Courtieu
2014-12-15Changed bullet informations to warning for better display in PG.Pierre Courtieu
2014-11-27Feedback: API cleaned up, documented and made user extensibleEnrico Tassi
2014-11-10Plug the dynamic tags in the Richpp mechanism.Pierre-Marie Pédrot
2014-11-10Adding a dynamic tag type in Pp.Pierre-Marie Pédrot
2014-11-04lib/Pp.tag: New.Regis-Gianas
2014-11-04lib/Pp.rewrite: New.Regis-Gianas