From 5ac6c86ad8e18161151d53687da1e2825f0a6b46 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 13 Oct 2016 13:49:04 +0200
Subject: [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.
---
 test-suite/output/Arguments_renaming.out | 6 ++++--
 test-suite/output/ltac.out               | 3 ++-
 2 files changed, 6 insertions(+), 3 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index 1633ad9765..e665db47d5 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 f4254e4e2f..a2d545202d 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
-- 
cgit v1.2.3