aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/print.ml
Commit message (Collapse)AuthorAge
* [checker] Printer cleanup.Gravatar Emilio Jesus Gallego Arias2018-03-07
| | | | Makes printing rules more explicit and should close #6799.
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* [checker] Fix/fine tune printing.Gravatar Emilio Jesus Gallego Arias2016-08-18
| | | | | | | | | | | | | | | | | | | | | In 91ee24b4a7843793a84950379277d92992ba1651 , we discouraged direct access to the console, recommending instead to provide information to the user by means of the `Feedback.msg_*` facilities. However, we introduced a display bug in the checker printer as it is special and doesn't use the Pp facilities (likely for trust reasons), spotted by @herbelin This patch fixes this bug and performs a couple more of fine tunings in the input. However, it could be desirable to port the `checker/printer.ml` to `Pp` and use the feedback mechanism; this would allow IDEs to use the checker in a more convenient way, at the cost of trusting `Pp` (which is already a bit trusted currently) A start of that idea can be found at: https://github.com/ejgallego/coq/tree/fix_checker_printing
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | This patch splits pretty printing representation from IO operations. - `Pp` is kept in charge of the abstract pretty printing representation. - The `Feedback` module provides interface for doing printing IO. The patch continues work initiated for 8.5 and has the following effects: - The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`, `pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`, `msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be used instead. - Feedback provides different backends to handle output, currently, `stdout`, `emacs` and CoqIDE backends are provided. - Clients cannot specify flush policy anymore, thus `pp_flush` et al are gone. - `Feedback.feedback` takes an `edit_or_state_id` instead of the old mix. Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.
* Checker: avoid using obsolete names from NamesGravatar Pierre Letouzey2016-05-31
|
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
|
* Checker: Fix bug #4282Gravatar Matthieu Sozeau2015-07-07
| | | | | Adapt to new [projection] abstract type comprising a constant and a boolean.
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Adapt the checker to polymorphic universes and projections (untested).Gravatar Matthieu Sozeau2014-05-08
|
* printer for coqchkGravatar Enrico Tassi2014-04-08