diff options
| author | Arnaud Spiwack | 2013-12-09 14:36:30 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2013-12-09 14:36:30 +0100 |
| commit | 0b4de5132a8fcda6dafe836dd249a4fc69b400fc (patch) | |
| tree | 70e7e98bb47d4cebdf8aa2bccb11bac14dbfc8ab /kernel/nativecode.ml | |
| parent | d3a6453f1447bfb956547050ddbd005f4b4751b6 (diff) | |
Fix printing of Ltac's backtrace.
I used an exception wrapper to report Tactic failures. It had the consequence of making process_vernac_interp_error to look for the backtrace at the wrong place.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions