diff options
| author | Hugo Herbelin | 2020-07-29 17:59:35 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-08-18 10:33:51 +0200 |
| commit | 05eb5d91989c0d0c470a1b35af52c84a60853f89 (patch) | |
| tree | 98a50807d4a622c8b78ef247fe1dc391b6dbdba5 /kernel/type_errors.mli | |
| parent | aa926429727f1f6b5ef07c8912f2618d53f6d155 (diff) | |
Remaining bugs in PR#12223 which fixed location of tactic errors (issue #12152).
The update of a loc needs sometimes to override (when calling an Ltac
function), and otherwise to keep the existing loc (assumed to be
fined). We refine this (see e.g. the ErrorLocation_tac_in_term tests).
Moreover, when overriding, this was going to a tclOR backtracking
point which was setting the loc to a completely disjoint part of the
code having caused the error (see #12773). We replace the tclOR by a
tclORELSE.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions