[checker] Fix/fine tune printing.

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

0 files changed, 0 insertions, 0 deletions