From 63cfc77ddf3586262d905dc351b58669d185a55e Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 31 Mar 2017 20:38:52 +0200
Subject: [toplevel] Remove exception error printer in favor of feedback
 printer.

We solve https://coq.inria.fr/bugs/show_bug.cgi?id=4789 by printing
all the errors from the feedback handler, even in the case of coqtop.

All error display is handled by a single, uniform path.

There may be some minor discrepancies with 8.6 as we are uniform now
whereas 8.6 tended to print errors in several ways, but our behavior
is a subset of the 8.6 behavior.

We had to make a choice for `-emacs` error output, which used to vary
too. We have chosen to display error messages as:

```
(location info) option \n
(program caret) option \n
MARKER[254]Error: msgMARKER[255]
```

This commit also fixes:

- https://coq.inria.fr/bugs/show_bug.cgi?id=5418
- https://coq.inria.fr/bugs/show_bug.cgi?id=5429
---
 test-suite/output/ErrorInModule.out | 1 +
 1 file changed, 1 insertion(+)

(limited to 'test-suite/output/ErrorInModule.out')

diff --git a/test-suite/output/ErrorInModule.out b/test-suite/output/ErrorInModule.out
index 851ecd9306..776dfeb550 100644
--- a/test-suite/output/ErrorInModule.out
+++ b/test-suite/output/ErrorInModule.out
@@ -1,2 +1,3 @@
 File "stdin", line 3, characters 20-31:
 Error: The reference nonexistent was not found in the current environment.
+
-- 
cgit v1.2.3