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 /test-suite | |
| 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')
| -rw-r--r-- | test-suite/output/Arguments_renaming.out | 6 | ||||
| -rw-r--r-- | test-suite/output/ltac.out | 3 |
2 files changed, 6 insertions, 3 deletions
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 1633ad976..e665db47d 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -2,7 +2,8 @@ File "stdin", line 1, characters 0-36: Warning: Ignoring rename of x into y. Only implicit arguments can be renamed. [arguments-ignore-rename-nonimpl,vernacular] The command has indeed failed with message: -Error: To rename arguments the "rename" flag must be specified. +Error: +To rename arguments the "rename" flag must be specified. Argument A renamed to B. File "stdin", line 2, characters 0-25: Warning: Ignoring rename of A into T. Only implicit arguments can be renamed. @@ -125,5 +126,6 @@ File "stdin", line 53, characters 0-26: Warning: Ignoring rename of x into s. Only implicit arguments can be renamed. [arguments-ignore-rename-nonimpl,vernacular] The command has indeed failed with message: -Error: To rename arguments the "rename" flag must be specified. +Error: +To rename arguments the "rename" flag must be specified. Argument A renamed to R. 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 |