diff options
| author | Emilio Jesus Gallego Arias | 2017-04-24 18:42:03 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-04-24 19:54:00 +0200 |
| commit | da0d6da035206778c1d99ef51f471b4b22016492 (patch) | |
| tree | 088dfba93de0bdf155f31316c3f54b8222bbf12a /kernel | |
| parent | e57074289193b0f0184f3c7143d8ab7e0edd5112 (diff) | |
[toplevel] Don't mask critical exceptions in vernac interpretation.
Indeed we were not correctly backtracking in the case of
StackOverflow. It makes sense to remove the inner handler which is a
leftover of a previous attempt, and handle interpretation errors in
load as non-recoverable.
This fixes: https://coq.inria.fr/bugs/show_bug.cgi?id=5485
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions