index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
lib
/
pp.mli
Age
Commit message (
Expand
)
Author
2019-06-17
Update ml-style headers to new year.
Théo Zimmermann
2019-05-23
Fixing typos - Part 3
JPR
2019-05-23
Fixing typos - Part 2
JPR
2018-10-06
[api] Remove (most) 8.9 deprecated objects.
Emilio Jesus Gallego Arias
2018-07-23
Displays the differences between successive proof steps in coqtop and CoqIDE.
Jim Fehrle
2018-02-27
Update headers following #6543.
Théo Zimmermann
2017-12-12
Improving spacing in printing disjunctive patterns.
Hugo Herbelin
2017-07-27
deprecate Pp.std_ppcmds type alias
Matej Košík
2017-07-12
format pairs of items for pr_depth to get alternating separators
Paul Steckler
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2017-06-07
completing a sentence in a comment
Matej 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-20
Merge PR#189: Remove tabulation support from pretty-printing.
Maxime Dénès
2016-10-12
Merge PR #224 into v8.6
Pierre-Marie Pédrot
2016-10-09
Moving Pp.comments to CLexer so that Pp is purer (no more side-effect
Hugo Herbelin
2016-09-30
[pp] Remove duplicate color logger.
Emilio Jesus Gallego Arias
2016-06-29
A new infrastructure for warnings.
Maxime Dénès
2016-06-02
Add documentation to the low-level `Pp` functions.
Emilio Jesus Gallego Arias
2016-06-02
Remove tabulation support from pretty-printing.
Guillaume Melquiond
2016-05-31
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-09
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-05-04
typo
Enrico Tassi
2016-04-09
In pr_clauses, do not print a leading space by default so that it can
Hugo Herbelin
2016-01-21
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-20
Update copyright headers.
Maxime Dénès
2015-09-20
Rich printing of messages.
Pierre-Marie Pédrot
2015-05-04
Add a [Redirect] vernacular command
Clément Pit--Claudel
2015-04-23
Removing dead code in Pp.
Pierre-Marie Pédrot
2015-01-12
Update headers.
Maxime Dénès
2014-12-16
msg_info now puts infomsg tag in emacs mode.
Pierre Courtieu
2014-12-15
Changed bullet informations to warning for better display in PG.
Pierre Courtieu
2014-11-27
Feedback: API cleaned up, documented and made user extensible
Enrico Tassi
2014-11-10
Plug the dynamic tags in the Richpp mechanism.
Pierre-Marie Pédrot
2014-11-10
Adding a dynamic tag type in Pp.
Pierre-Marie Pédrot
2014-11-04
lib/Pp.tag: New.
Regis-Gianas
2014-11-04
lib/Pp.rewrite: New.
Regis-Gianas
2014-11-04
lib/Pp: Publish combinators for tags opening and closing.
Regis-Gianas
[next]