diff options
author | 2016-10-13 13:49:04 +0200 | |
---|---|---|
committer | 2016-10-18 21:56:56 +0200 | |
commit | 5ac6c86ad8e18161151d53687da1e2825f0a6b46 (patch) | |
tree | c8503040a7ed852425fede1e1fc5a25755619383 /test-suite/output/ltac.out | |
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 'test-suite/output/ltac.out')
-rw-r--r-- | test-suite/output/ltac.out | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out index f4254e4e2..a2d545202 100644 --- a/test-suite/output/ltac.out +++ b/test-suite/output/ltac.out @@ -1,5 +1,6 @@ The command has indeed failed with message: -Error: Ltac variable y depends on pattern variable name z which is not bound in current context. +Error: +Ltac variable y depends on pattern variable name z which is not bound in current context. Ltac f x y z := symmetry in x, y; auto with z; auto; intros **; clearbody x; generalize dependent z |