diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-07-20 00:12:01 +0200 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2017-09-21 16:53:15 +0200 |
| commit | 18250a35127ed8913dd05f31f109b308a0f11826 (patch) | |
| tree | a1a5954b494542246d8d058e9c63311f34111982 /tactics/dn.ml | |
| parent | 9933871efd122163f7e2dfe8377b9b2dd384b47b (diff) | |
[checker] Add missing Feedback printer (BZ#5587)
This fixes longstanding bug likely introduced in the first `pp` to
`Feedback` migration, namely the checker didn't register a feedback
printer, thus no calls to `Feedback.msg_*` were printed in the
checker.
This closes bug: https://coq.inria.fr/bugs/show_bug.cgi?id=5587
We fix this by adding a custom printer to the checker, this is correct
as the checker owns now the full console, however a cleanup should
happen in any of these two directions:
- all the calls to feedback are removed, and the checker always uses
its own printing mechanism.
- all the calls to `Format/Printf` are removed and the checker always
uses the `Feedback` mechanism.
Currently, I have no opinion on this.
Diffstat (limited to 'tactics/dn.ml')
0 files changed, 0 insertions, 0 deletions