diff options
| author | Emilio Jesus Gallego Arias | 2017-04-24 19:25:48 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-04-25 18:43:03 +0200 |
| commit | 4abb41d008fc754f21916dcac9cce49f2d04dd6d (patch) | |
| tree | 3823e5c3706386d8bf997b5d8d25b42b81f2347d /kernel/nativecode.ml | |
| parent | 0fd7d060e0872a6ae3662dfb7a1fb940b80ef9df (diff) | |
[toplevel] Use exception information for error printing.
This is a partial backtrack on
63cfc77ddf3586262d905dc351b58669d185a55e. In that commit, we
disregarded exception and tried to print error messages just by
listening to feedback.
However, feedback error messages are not always emitted due to
https://coq.inria.fr/bugs/show_bug.cgi?id=5479
Thus meanwhile it is safer to go back to printing the information
present in exceptions until we tweak the STM.
This fixes https://coq.inria.fr/bugs/show_bug.cgi?id=5467 and many
other glitches not reported, such errors in nested proofs.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions