aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/topfmt.ml
Commit message (Expand)AuthorAge
* Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\
| * Post-rebase warnings (unused opens and 2 unused values)Gravatar Gaetan Gilbert2017-04-27
| * Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
| * [toplevel] Use exception information for error printing.Gravatar Emilio Jesus Gallego Arias2017-04-25
* | [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
|/
* [toplevel] [emacs] Don't quote errors in emacs mode.Gravatar Emilio Jesus Gallego Arias2017-04-23
* [toplevel] Fix #5475Gravatar Emilio Jesus Gallego Arias2017-04-18
* [toplevel] Remove exception error printer in favor of feedback printer.Gravatar Emilio Jesus Gallego Arias2017-04-05
* [pp] Add anomaly header to anomaly error messages.Gravatar Emilio Jesus Gallego Arias2017-03-22
* [pp] Move terminal-specific tagging to the toplevel.Gravatar Emilio Jesus Gallego Arias2017-03-21
* [pp] Remove special tag type and handler from Pp.Gravatar Emilio Jesus Gallego Arias2017-03-21
* [pp] Make feedback the only logging mechanism.Gravatar Emilio Jesus Gallego Arias2017-03-21
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 04:22:56 +0000