diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-10-13 13:49:04 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-10-18 21:56:56 +0200 |
| commit | 5ac6c86ad8e18161151d53687da1e2825f0a6b46 (patch) | |
| tree | c8503040a7ed852425fede1e1fc5a25755619383 /plugins/ssrmatching | |
| parent | 7ff42d43a6107dff984676902943ec32f187c40d (diff) | |
[pp] Try to properly tag error messages in cError.
In order to get proper coloring, we must tag the headers of error
messages in `CError`.
This should fix bug
https://coq.inria.fr/bugs/show_bug.cgi?id=5135
However, note that this could interact badly with the richpp printing
used by the IDE. At this level, we have no clue which tag we'd like to
apply, as we know (and shouldn't) nothing about the top level backend.
Thus, for now I've selected the console printer, hoping that the
`Richpp` won't crash the IDE.
Diffstat (limited to 'plugins/ssrmatching')
0 files changed, 0 insertions, 0 deletions