aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/topfmt.ml
Commit message (Expand)AuthorAge
* [nit] Remove some unnecessary global `open Feedback`Gravatar Emilio Jesus Gallego Arias2018-02-09
* [toplevel] Properly redirect stdout on `Redirect` vernac.Gravatar Emilio Jesus Gallego Arias2017-11-28
* Using an algebraic type for distinguishing toplevel input from location in file.Gravatar Hugo Herbelin2017-09-14
* Adding support for bindings tags to explicit prefix/suffix rather than colors.Gravatar Hugo Herbelin2017-07-08
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* 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-12-04 00:23:13 +0000