diff options
| author | Hugo Herbelin | 2020-09-09 12:58:41 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-09-16 08:08:18 +0200 |
| commit | fc0aa1e70cb1891ef3f62566af4e551d06bfb613 (patch) | |
| tree | bda03cc9cd546c2c7355f9f6ff893bd6612a9e51 /kernel/nativelib.mli | |
| parent | d6b6e1d6ceadfe65ea398786361ff7737624deaf (diff) | |
More improvements in locating tactic errors.
We finally pass the location in the "ist", and keep it in the "VFun"
which is associated to expanded Ltac constants.
Diffstat (limited to 'kernel/nativelib.mli')
0 files changed, 0 insertions, 0 deletions